Commit 2023-06-29 05:08 6ac87310

View on Github →

feat: add lemmas about AffineSubspacec (#5570)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

added theorem AffineSubspace.comap_bot

added theorem Submodule.mem_toAffineSubspace

added theorem Submodule.toAffineSubspace_direction