Theorem Submodule.toAffineSubspace_direction

Modification history

2023-06-29 05:08
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
feat: add lemmas about `AffineSubspace`c (#5570)
Added Submodule.toAffineSubspace_directionView on Github →