Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use ZeroLEOneClass #9250

Closed
wants to merge 27 commits into from
Closed

chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use ZeroLEOneClass #9250

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
20e8ce1
feat: synchronize with mathlib3 #16525
FR-vdash-bot Nov 29, 2022
c3eacbc
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Dec 24, 2022
71b978e
Update Defs.lean
FR-vdash-bot Dec 24, 2022
1570ce6
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Dec 23, 2023
46548cf
ported from https://github.com/leanprover-community/mathlib/pull/18158
FR-vdash-bot Dec 23, 2023
a5e5161
fix
FR-vdash-bot Dec 24, 2023
a39cc94
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot May 16, 2024
5260861
fix
FR-vdash-bot May 17, 2024
3117a46
fix
FR-vdash-bot May 17, 2024
ba4c3ce
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot May 23, 2024
73eff91
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Jul 13, 2024
90b1b4f
deprecated
FR-vdash-bot Jul 13, 2024
ccd7635
more
FR-vdash-bot Jul 13, 2024
ca1ba0e
fix
FR-vdash-bot Jul 13, 2024
5c11cfe
fix
FR-vdash-bot Jul 13, 2024
0de833f
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Jul 17, 2024
dfe66c9
fix
FR-vdash-bot Jul 17, 2024
b1d0835
alias
FR-vdash-bot Jul 17, 2024
8cead35
move
FR-vdash-bot Jul 17, 2024
d1281d0
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Jul 24, 2024
7eb3c36
shorter name
FR-vdash-bot Jul 25, 2024
5583087
deprecated alias
FR-vdash-bot Jul 25, 2024
4702966
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Aug 3, 2024
5fa0cca
fix
FR-vdash-bot Aug 3, 2024
83b55a1
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Aug 27, 2024
c53fc99
fix merge
FR-vdash-bot Aug 27, 2024
09a72c1
Merge branch 'master' into FR_order_refactor18
FR-vdash-bot Oct 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Archive/Wiedijk100Theorems/BuffonsNeedle.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ lemma short_needle_inter_eq (h : l ≤ d) (θ : ℝ) :
Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2) := by
rw [Set.Icc_inter_Icc, inf_eq_min, sup_eq_max, max_div_div_right zero_le_two,
min_div_div_right zero_le_two, neg_mul, max_neg_neg, mul_comm,
min_eq_right (mul_le_of_le_of_le_one_of_nonneg h θ.sin_le_one hl.le)]
min_eq_right ((mul_le_of_le_one_right hl.le θ.sin_le_one).trans h)]

include hd hBₘ hB hl in
/--
Expand Down
Loading
Loading