Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.supr_eq_to_submodule_range

Modification history

2022-01-31 14:14
src/algebra/direct_sum/internal.lean
feat(linear_algebra/{tensor,exterior,clifford}_algebra): these algebras are graded by powers of the submodules of their generators (#11542) …
Added submodule.supr_eq_to_submodule_rangeView on Github →