Commit 2023-01-23 12:02 cff6012d

View on Github →

chore: tidy various files (#1693)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

added theorem Finset.prod_natCast

deleted theorem Finset.prod_nat_cast

Modified Mathlib/Algebra/Order/Monoid/Lemmas.lean

added theorem Antitone.mul_strictAnti'

deleted theorem Antitone.mul_strict_anti'

added theorem AntitoneOn.mul_strictAnti'

deleted theorem AntitoneOn.mul_strict_anti'

added theorem Monotone.mul_strictMono'

deleted theorem Monotone.mul_strict_mono'

added theorem MonotoneOn.mul_strictMono'

deleted theorem MonotoneOn.mul_strict_mono'

added theorem bit0_strictMono

deleted theorem bit0_strict_mono

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.consCases_cons

deleted theorem Fin.cons_cases_cons

Modified Mathlib/Data/Fintype/Card.lean

modified theorem Finite.exists_univ_list

modified theorem Finite.of_injective

added theorem Fintype.card_ofFinset

added theorem Fintype.card_ofSubsingleton

deleted theorem Fintype.card_of_finset

added theorem Fintype.card_of_isEmpty

deleted theorem Fintype.card_of_is_empty

deleted theorem Fintype.card_of_subsingleton

added theorem Fintype.card_orderDual

deleted theorem Fintype.card_order_dual

Modified Mathlib/Data/Fintype/Powerset.lean

Modified Mathlib/Data/Nat/Fib.lean

added theorem Nat.fib_add_two_strictMono

deleted theorem Nat.fib_add_two_strict_mono

Modified Mathlib/Data/Real/Sign.lean

modified theorem Real.sign_apply_eq_of_ne_zero

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/Data/Vector/Basic.lean

added theorem Vector.nth_eq_nthLe

deleted theorem Vector.nth_eq_nth_le

modified theorem Vector.scanl_head

modified theorem Vector.scanl_singleton

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

added theorem Submonoid.comap_strictMono_of_surjective

deleted theorem Submonoid.comap_strict_mono_of_surjective

added theorem Submonoid.map_strictMono_of_injective

deleted theorem Submonoid.map_strict_mono_of_injective

Modified Mathlib/Order/Grade.lean

added theorem grade_strictMono

deleted theorem grade_strict_mono