Commit 2026-03-19 10:06 37920956

View on Github →

feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections (#33348)

LinearEquiv.fixedReduce. Pass a linear equivalence to the quotient by a fixed subspace.
Characterize transvections among dilatransvections by the fact that their reduction is the identity.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

added theorem Submodule.mem_stabilizer_submodule_iff_map_eq

added theorem Submodule.pointwise_smul_def

added theorem Submodule.stabilizer_coe

Modified Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

added theorem Submodule.sup_span_singleton_eq_top_iff

Created Mathlib/LinearAlgebra/FixedSubmodule.lean

added def LinearEquiv.fixedReduce

added theorem LinearEquiv.fixedReduce_eq_one

added theorem LinearEquiv.fixedReduce_eq_smul_iff

added theorem LinearEquiv.fixedReduce_mk

added theorem LinearEquiv.fixedReduce_mkQ

added theorem LinearEquiv.fixedSubmodule_eq_top_iff

added theorem LinearEquiv.map_eq_of_mem_fixingSubgroup

added theorem LinearEquiv.mem_stabilizer_fixedSubmodule

added theorem LinearEquiv.mem_stabilizer_submodule_of_le_fixedSubmodule

added def LinearEquiv.reduce

added theorem LinearEquiv.reduce_mk

added theorem LinearEquiv.reduce_mkQ

added def LinearMap.fixedSubmodule

added theorem LinearMap.fixedSubmodule_comp_inf_fixedSubmodule_le

added theorem LinearMap.fixedSubmodule_eq_ker

added theorem LinearMap.fixedSubmodule_eq_top_iff

added theorem LinearMap.fixedSubmodule_inf_fixedSubmodule_le_comp

added theorem LinearMap.mem_fixedSubmodule_iff

Modified Mathlib/LinearAlgebra/Transvection.lean

deleted theorem LinearMap.transvection.IsBaseChange.transvection

added theorem LinearMap.transvection.LinearEquiv.IsBaseChange.transvection

added theorem LinearMap.transvection.LinearEquiv.LinearEquiv.dilatransvection.baseChange

added theorem LinearMap.transvection.LinearEquiv.LinearEquiv.transvection.baseChange

added theorem LinearMap.transvection.LinearEquiv.LinearMap.transvection.baseChange

added theorem LinearMap.transvection.LinearEquiv.LinearMap.transvection.det

deleted theorem LinearMap.transvection.LinearEquiv.dilatransvection.baseChange

added theorem LinearMap.transvection.LinearEquiv.ker_le_fixedSubmodule_transvection

modified theorem LinearMap.transvection.LinearEquiv.mem_dilatransvections_iff_finrank

added theorem LinearMap.transvection.LinearEquiv.mem_dilatransvections_iff_finrank_quotient

modified theorem LinearMap.transvection.LinearEquiv.mem_dilatransvections_iff_rank

added theorem LinearMap.transvection.LinearEquiv.mem_dilatransvections_iff_rank_quotient

added theorem LinearMap.transvection.LinearEquiv.mem_fixedSubmodule_transvection_iff

added theorem LinearMap.transvection.LinearEquiv.mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one

deleted theorem LinearMap.transvection.LinearEquiv.transvection.baseChange

added theorem LinearMap.transvection.LinearEquiv.transvection_mem_dilatransvections

added theorem LinearMap.transvection.LinearEquiv.transvection_mem_transvections

deleted theorem LinearMap.transvection.LinearMap.transvection.baseChange

deleted theorem LinearMap.transvection.LinearMap.transvection.det

Modified Mathlib/RingTheory/Regular/RegularSequence.lean