Theorem Submodule.toAffineSubspace_inj

Modification history

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