Commit 2024-10-29 16:55 07a7b10f

View on Github →

chore(LinearAlgebra): split Quotient.lean into Defs and Basic (#18384) This PR rearranges the definitions of quotient modules as follows:

  • LinearAlgebra/QuotientPi.lean is renamed LinearAlgebra/Quotient/Pi.lean
  • LinearAlgebra/Quotient.lean is split into
    • LinearAlgebra/Quotient/Defs.lean (with the definition and module structure of the quotient module)
    • LinearAlgebra/Quotient/Basic.lean (with some basic maps for the quotient)

Estimated changes

deleted theorem Submodule.Quotient.mk_add
deleted theorem Submodule.Quotient.mk_neg
deleted theorem Submodule.Quotient.mk_sub
deleted theorem Submodule.linearMap_qext
deleted def Submodule.mkQ
deleted theorem Submodule.mkQ_apply
deleted theorem Submodule.mkQ_surjective
deleted theorem Submodule.quot_hom_ext
deleted theorem Submodule.quotientRel_def
added def Submodule.mkQ
added theorem Submodule.mkQ_apply
added theorem Submodule.quot_hom_ext