Theorem Submodule.toAffineSubspace_injective

Modification history

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