Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-30 16:49 d420db54

View on Github →

chore(algebra/algebra): trivial lemmas for alg_equiv (#8139)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_equiv.coe_alg_hom_injective

added theorem alg_equiv.coe_alg_hom_of_alg_hom

modified theorem alg_equiv.coe_ring_equiv_injective

added theorem alg_equiv.of_alg_hom_coe_alg_hom

added theorem alg_equiv.of_alg_hom_symm

deleted theorem alg_equiv.of_linear_equiv_apply

added theorem alg_equiv.of_linear_equiv_symm

deleted theorem alg_equiv.to_linear_equiv_inj

added theorem alg_equiv.to_linear_equiv_injective

deleted theorem alg_equiv.to_linear_map_inj

added theorem alg_equiv.to_linear_map_injective

deleted theorem alg_hom.to_linear_map_inj

added theorem alg_hom.to_linear_map_injective

Modified src/algebra/monoid_algebra.lean

Modified src/ring_theory/tensor_product.lean