Commit 2024-09-28 17:13 5cd5bfff

View on Github →

chore: rename Submodule.coeSubtype (#17219)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/Algebra/Lie/EngelSubalgebra.lean

Modified Mathlib/Algebra/Lie/Semisimple/Basic.lean

Modified Mathlib/Algebra/Lie/Weights/Cartan.lean

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

deleted theorem Submodule.coeSubtype

added theorem Submodule.coe_subtype

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

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

Modified Mathlib/Algebra/Star/Module.lean

Modified Mathlib/Analysis/Calculus/Implicit.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/LinearAlgebra/Projection.lean

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

Modified Mathlib/NumberTheory/NumberField/FractionalIdeal.lean

Modified Mathlib/Probability/ConditionalExpectation.lean

Modified Mathlib/RingTheory/Flat/Basic.lean