Commit 2026-10-20 16:12 e8bc55fd

View on Github →

feat: lattice lemmas about Submodule.toAffineSubspace (#43415)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

added theorem Submodule.monotone_toAffineSubspace

added theorem Submodule.toAffineSubspace_bot

added theorem Submodule.toAffineSubspace_iInf

added theorem Submodule.toAffineSubspace_iSup

added theorem Submodule.toAffineSubspace_inf

added theorem Submodule.toAffineSubspace_inj

added theorem Submodule.toAffineSubspace_injective

added theorem Submodule.toAffineSubspace_le_toAffineSubspace

added theorem Submodule.toAffineSubspace_sInf

added theorem Submodule.toAffineSubspace_sSup

added theorem Submodule.toAffineSubspace_sup

added theorem Submodule.toAffineSubspace_top