Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-01 09:09 bf0f15ab

View on Github →

chore(algebra/algebra/basic): add missing lemmas (#7412)

Estimated changes

Modified src/algebra/algebra/basic.lean

modified theorem alg_equiv.coe_refl

added theorem alg_equiv.coe_trans

added theorem alg_equiv.left_inverse_symm

added theorem alg_equiv.refl_to_alg_hom

added theorem alg_equiv.right_inverse_symm

modified theorem alg_equiv.trans_apply

added theorem alg_hom.coe_comp

added theorem alg_hom.coe_id

modified theorem alg_hom.comp_apply

added theorem alg_hom.comp_to_ring_hom

modified theorem alg_hom.id_apply

added theorem alg_hom.id_to_ring_hom