Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 16:35 1b787d6b

View on Github →

feat(linear_algebra/span): generalize span_singleton_smul_eq (#12736)

Estimated changes

Modified src/analysis/inner_product_space/projection.lean

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/projective_space/basic.lean

Modified src/linear_algebra/span.lean

added theorem submodule.span_singleton_group_smul_eq

modified theorem submodule.span_singleton_smul_eq

modified theorem submodule.span_singleton_smul_le