Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.eq_top_of_disjoint

Modification history

2020-08-23 02:34

src/linear_algebra/finite_dimensional.lean

feat(linear_algebra/finite_dimensional): Add `linear_equiv.of_inj_endo` and related lemmas (#3878) …

Added submodule.eq_top_of_disjoint View on Github →