Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-14 09:32 bca82787

View on Github →

feat(algebra/lie/basic): add missing @[ext] and @[simp] lemmas (#10316)

Estimated changes

Modified src/algebra/lie/basic.lean

deleted theorem lie_equiv.bijective

added theorem lie_equiv.coe_injective

added theorem lie_equiv.coe_linear_equiv_injective

deleted theorem lie_equiv.coe_to_lie_equiv

added theorem lie_equiv.coe_to_lie_hom

added theorem lie_equiv.ext

deleted theorem lie_equiv.injective

added theorem lie_equiv.self_trans_symm

deleted theorem lie_equiv.surjective

added theorem lie_equiv.symm_trans

deleted theorem lie_equiv.symm_trans_apply

added theorem lie_equiv.symm_trans_self

added theorem lie_equiv.to_linear_equiv_mk

added theorem lie_module_equiv.self_trans_symm

added theorem lie_module_equiv.symm_trans

deleted theorem lie_module_equiv.symm_trans_apply

added theorem lie_module_equiv.symm_trans_self

Modified src/data/equiv/module.lean

added theorem linear_equiv.coe_injective