Theorem Submodule.toAffineSubspace_le_toAffineSubspace

Modification history

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