Mathlib Changelog
Changelog
About
Github
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