Commit 2024-06-24 20:33 88693717

View on Github →

chore: move linear equivalences about submodules to Algebra.Module.Submodule.Equiv (#13684)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Algebra/Unitization.lean

Modified Mathlib/Algebra/Lie/Basic.lean

Created Mathlib/Algebra/Module/Submodule/Equiv.lean

added theorem LinearEquiv.coe_ofEq_apply

added theorem LinearEquiv.coe_ofTop_symm_apply

added theorem LinearEquiv.eq_bot_of_equiv

added theorem LinearEquiv.ofBijective_apply

added theorem LinearEquiv.ofBijective_symm_apply_apply

added def LinearEquiv.ofEq

added theorem LinearEquiv.ofEq_rfl

added theorem LinearEquiv.ofEq_symm

added theorem LinearEquiv.ofInjective_apply

added def LinearEquiv.ofLeftInverse

added theorem LinearEquiv.ofLeftInverse_apply

added theorem LinearEquiv.ofLeftInverse_symm_apply

added def LinearEquiv.ofSubmodule'

added theorem LinearEquiv.ofSubmodule'_apply

added theorem LinearEquiv.ofSubmodule'_symm_apply

added theorem LinearEquiv.ofSubmodule'_toLinearMap

added def LinearEquiv.ofSubmodules

added theorem LinearEquiv.ofSubmodules_apply

added theorem LinearEquiv.ofSubmodules_symm_apply

added def LinearEquiv.ofTop

added theorem LinearEquiv.ofTop_apply

added theorem LinearEquiv.ofTop_symm_apply

added theorem LinearEquiv.range_comp

added def Submodule.equivSubtypeMap

added theorem Submodule.equivSubtypeMap_apply

added theorem Submodule.equivSubtypeMap_symm_apply

Modified Mathlib/Analysis/Convex/Star.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem LinearEquiv.coe_ofEq_apply

deleted theorem LinearEquiv.coe_ofTop_symm_apply

deleted theorem LinearEquiv.eq_bot_of_equiv

deleted theorem LinearEquiv.ofBijective_apply

deleted theorem LinearEquiv.ofBijective_symm_apply_apply

deleted def LinearEquiv.ofEq

deleted theorem LinearEquiv.ofEq_rfl

deleted theorem LinearEquiv.ofEq_symm

deleted theorem LinearEquiv.ofInjective_apply

deleted def LinearEquiv.ofLeftInverse

deleted theorem LinearEquiv.ofLeftInverse_apply

deleted theorem LinearEquiv.ofLeftInverse_symm_apply

deleted def LinearEquiv.ofSubmodule'

deleted theorem LinearEquiv.ofSubmodule'_apply

deleted theorem LinearEquiv.ofSubmodule'_symm_apply

deleted theorem LinearEquiv.ofSubmodule'_toLinearMap

deleted def LinearEquiv.ofSubmodules

deleted theorem LinearEquiv.ofSubmodules_apply

deleted theorem LinearEquiv.ofSubmodules_symm_apply

deleted def LinearEquiv.ofTop

deleted theorem LinearEquiv.ofTop_apply

deleted theorem LinearEquiv.ofTop_symm_apply

deleted theorem LinearEquiv.range_comp

deleted def Submodule.equivSubtypeMap

deleted theorem Submodule.equivSubtypeMap_apply

deleted theorem Submodule.equivSubtypeMap_symm_apply

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Matrix/Circulant.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/LinearAlgebra/Prod.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/Span.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

Modified scripts/noshake.json