Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-18 12:23 ffb99a33

View on Github →

chore(algebra/group/type_tags): add additive.to_mul etc (#2363) Don't make additive and multiplicative irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from ℕ, ℤ and their multiplicative versions are defined by the image of 1.

Estimated changes

added def additive.of_mul
added def additive.to_mul
added theorem of_add_add
added theorem of_add_inj
added theorem of_add_neg
added theorem of_add_to_add
added theorem of_add_zero
added theorem of_mul_inj
added theorem of_mul_inv
added theorem of_mul_mul
added theorem of_mul_one
added theorem of_mul_to_mul
added theorem to_add_inj
added theorem to_add_inv
added theorem to_add_mul
added theorem to_add_of_add
added theorem to_add_one
added theorem to_mul_add
added theorem to_mul_inj
added theorem to_mul_neg
added theorem to_mul_of_mul
added theorem to_mul_zero
added def gmultiples_hom
added theorem gpow_of_add
added def gpowers_hom
added def multiples_hom
added theorem pow_of_add
added def powers_hom