Theorem DirectSum.lie_of_same

Modification history

2023-11-13 17:59

Mathlib/Algebra/Lie/DirectSum.lean

fix(Mathlib/Algebra/Lie/DirectSum): remove unused `R` argument from lemmas (#8388) …

Added DirectSum.lie_of_same View on Github →