Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-31 13:49 e0b2ad8f

View on Github →

chore(algebra/lie/quotient): golf some instances (#14480)

Estimated changes

Modified src/algebra/lie/quotient.lean

deleted def lie_submodule.quotient.action_as_endo_map_bracket

modified theorem lie_submodule.quotient.is_quotient_mk