Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-31 08:37 badeb48b

View on Github →

feat(data/equiv/algebra): change mul_equiv field to map_mul (#1287)

feat(data/equiv/algebra): bundle field for mul_equiv
adding docs
Update src/data/equiv/algebra.lean
Update src/data/equiv/algebra.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr

Estimated changes

Modified src/category_theory/endomorphism.lean

Modified src/data/equiv/algebra.lean

added def add_equiv.apply_symm_apply

added def add_equiv.map_add

added def add_equiv.map_zero

added def add_equiv.refl

added def add_equiv.symm

added def add_equiv.symm_apply_apply

added def add_equiv.to_add_monoid_hom

added theorem add_equiv.to_equiv_symm

added def add_equiv.trans

added def mul_equiv.apply_symm_apply

added def mul_equiv.map_mul

added def mul_equiv.map_one

added def mul_equiv.symm_apply_apply

added theorem mul_equiv.to_equiv_symm

added def mul_equiv.to_monoid_hom

Modified src/data/mv_polynomial.lean

Modified src/linear_algebra/basic.lean

Modified src/ring_theory/free_comm_ring.lean

Modified src/ring_theory/noetherian.lean