Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-08 21:01 67e19cd9

View on Github →

feat(src/ring_theory/algebra): define equivalence of algebras (#2625)

Estimated changes

Modified src/ring_theory/algebra.lean

added theorem alg_equiv.apply_symm_apply

added theorem alg_equiv.bijective

added theorem alg_equiv.coe_ring_equiv

added theorem alg_equiv.coe_to_alg_equiv

added theorem alg_equiv.commutes

added theorem alg_equiv.injective

added theorem alg_equiv.map_add

added theorem alg_equiv.map_mul

added theorem alg_equiv.map_neg

added theorem alg_equiv.map_one

added theorem alg_equiv.map_sub

added theorem alg_equiv.map_zero

added def alg_equiv.refl

added theorem alg_equiv.surjective

added def alg_equiv.symm

added theorem alg_equiv.symm_apply_apply

added def alg_equiv.trans

added structure alg_equiv