Commit 2024-09-16 08:22 0f630816

View on Github →

feat: missing basic API lemmas (#16842)

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.cast_eq_zero

added theorem Fin.cast_injective

Modified Mathlib/Data/Fintype/Card.lean

added theorem Fin.val_eq_val_of_heq

Modified Mathlib/Data/Set/Function.lean

added theorem Function.apply_eq_of_range_eq_singleton

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/Order/Fin/Basic.lean

added theorem Fin.cast_strictMono

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Nat.card_range_of_injective

added theorem Nat.card_univ

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added theorem ContinuousLinearMap.comp_finset_sum

added theorem ContinuousLinearMap.finset_sum_comp

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

modified def ContinuousMultilinearMap.toContinuousLinearMap