Commit 2025-12-22 19:35 317e62e5

View on Github →

feat(LinearAlgebra/Transvection): auxiliary lemmas to compute the determinant of transvection in a module (#31138) Auxiliary results towards the proof that the determinant of a transvection is equal to 1.

Estimated changes

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem LinearMap.free_of_det_ne_one

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

added theorem TensorProduct.coe_finsuppScalarRight'

added theorem TensorProduct.finsuppScalarRight_smul

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

added theorem span_range_eq_top_iff_surjective_finsuppLinearCombination

added theorem span_range_eq_top_iff_surjective_fintypeLinearCombination

Modified Mathlib/LinearAlgebra/SpecialLinearGroup.lean

modified theorem SpecialLinearGroup.toLinearEquiv_apply

Modified Mathlib/LinearAlgebra/Transvection.lean

modified theorem IsBaseChange.transvection

modified theorem LinearMap.transvection.LinearEquiv.transvection.LinearMap.transvection.baseChange

modified theorem LinearMap.transvection.LinearEquiv.transvection.apply

modified theorem LinearMap.transvection.LinearEquiv.transvection.coe_apply

modified theorem LinearMap.transvection.LinearEquiv.transvection.coe_toLinearMap

modified theorem LinearMap.transvection.LinearEquiv.transvection.of_right_eq_zero

modified theorem LinearMap.transvection.LinearEquiv.transvection.symm_eq'

modified theorem LinearMap.transvection.LinearEquiv.transvection.symm_eq

modified theorem LinearMap.transvection.LinearEquiv.transvection.trans_of_left_eq

modified theorem LinearMap.transvection.LinearEquiv.transvection.trans_of_right_eq

modified def LinearMap.transvection.LinearEquiv.transvection

modified theorem LinearMap.transvection.apply

modified theorem LinearMap.transvection.comp_of_left_eq

modified theorem LinearMap.transvection.comp_of_left_eq_apply

modified theorem LinearMap.transvection.comp_of_right_eq

modified theorem LinearMap.transvection.comp_of_right_eq_apply

added theorem LinearMap.transvection.eq_id_of_finrank_le_one

modified theorem LinearMap.transvection.of_right_eq_zero

modified def LinearMap.transvection

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangeFree.lean

modified theorem IsBaseChange.free

added theorem IsBaseChange.of_basis

added theorem IsBaseChange.of_fintype_basis

added theorem IsBaseChange.of_fintype_basis_eq

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangeHom.lean

added theorem IsBaseChange.det_endHom

added theorem IsBaseChange.endHom_comp

added theorem IsBaseChange.endHom_comp_apply

added theorem IsBaseChange.endHom_one

added theorem IsBaseChange.endHom_toMatrix

added theorem IsBaseChange.linearMapLeftRightHom_toMatrix