Theorem LieSubmodule.independent_iff_coe_toSubmodule

Modification history

2024-11-25 10:13

Mathlib/Algebra/Lie/Submodule.lean

chore: rename `CompleteLattice.Independent`/`.SetIndependent` to `iSupIndep`/`sSupIndep` (#19409) …

Deleted LieSubmodule.independent_iff_coe_toSubmodule View on Github →

2023-11-20 21:32

Mathlib/Algebra/Lie/Submodule.lean

feat: if a Lie algebra has non-degenerate Killing form then its Cartan subalgebras are Abelian (#8430) …

Added LieSubmodule.independent_iff_coe_toSubmodule View on Github →