Theorem Submodule.toAffineSubspace_sInf

Modification history

2026-10-20 16:12
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
feat: lattice lemmas about `Submodule.toAffineSubspace` (#43415)
Added Submodule.toAffineSubspace_sInfView on Github →