feat(algebra/order/monoid_lemma_zero_lt): change tracking #16449
astrainfinita
wants to merge
28 commits into
master
from
FR_zero_lt_changes
feat(algebra/order/monoid_lemma_zero_lt): change tracking
09a68447
name issues after #16189
ae4d390d
#16099
4dd3cd43
#16102
45c70aff
#16097, style only
99d90ae6
#16447
293aefed
make it consistent again...
8e1befee
remove useless lemmas
37b8007d
deal with namespaces
b24c6f4c
use `₀` to avoid conflicts and replace lemmas in `algebra.order.ring`
2227ccc5
fix
a1a1eaab
remove `zero_lt` in other file
78e3224e
use `ₚ` instead of `₀`
e684fcdd
fix analysis/special_functions/bernstein
fe34c106
fix `number_theory/class_number/finite`
a19a5f5f
fix measure_theory\integral\set_to_l1
6cbbb12a
fix name
1e2fb18b
fix `apply_instance` failure (hack?)
ab1ef27a
fix `unify_with_instance` of tactic `mono`
5cd94681
fix test
1db16619
Merge branch 'master' into FR_zero_lt_changes
352af519
fix
b73501f5
Merge branch 'master' into FR_zero_lt_changes
1d73c31a
Update monoid_lemmas_zero_lt.lean
2fb682fe
Update monoid_lemmas_zero_lt.lean
578e38b3
Update monoid_lemmas_zero_lt.lean
4c2a0bd0
remove useless lemmas
b6f6a5d2
Update bernstein.lean
435f2bbe
Reviewers
No reviews
Assignees
No one assigned
Labels
t-algebra
t-order
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub