Commit 2023-12-11 22:56 e8acc5ce

View on Github →

feat: supporting lemmas for defining root systems (#8980) A collection of loosely-related lemmas, split out from other work in the hopes of simplifying review.

Estimated changes

Modified Mathlib/Algebra/Module/Basic.lean

added theorem CharZero.of_noZeroSMulDivisors

added theorem NoZeroSMulDivisors.int_of_charZero

Modified Mathlib/Algebra/Module/Equiv.lean

added theorem LinearEquiv.coe_one

added theorem LinearEquiv.coe_pow

added theorem LinearEquiv.coe_toLinearMap_mul

added theorem LinearEquiv.coe_toLinearMap_one

added theorem LinearEquiv.pow_apply

Modified Mathlib/Algebra/Module/LinearMap.lean

added theorem LinearMap.smulRight_apply_eq_zero_iff

added theorem LinearMap.smulRight_zero

added theorem LinearMap.zero_smulRight

Modified Mathlib/Data/Finite/Card.lean

added theorem Set.Finite.card_lt_card

added theorem Set.Finite.eq_of_subset_of_card_le

added theorem Set.Finite.equiv_image_eq_iff_subset

Modified Mathlib/Data/Set/Finite.lean

added theorem Set.Finite.injOn_iff_bijOn_of_mapsTo

added theorem Set.Finite.surjOn_iff_bijOn_of_mapsTo

Modified Mathlib/Data/Set/Function.lean

added theorem Equiv.image_eq_iff_bijOn

added theorem Set.MapsTo.coe_iterate_restrict

Modified Mathlib/Data/Set/Image.lean

added theorem Set.image_comp_eq

added theorem Set.image_id_eq

added theorem Set.image_iterate_eq

added theorem Set.image_mono

Modified Mathlib/Dynamics/FixedPoints/Basic.lean

added theorem Function.IsFixedPt.image_iterate

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem Function.Injective.isOfFinOrder_iff

Modified Mathlib/GroupTheory/Subgroup/ZPowers.lean

added theorem Int.zmultiples_one

Modified Mathlib/LinearAlgebra/Span.lean

added theorem Submodule.span_setOf_mem_eq_top