Commit 2024-11-23 00:05 4fe03b81

View on Github →

chore(Algebra/Group/TypeTags): Remove porting notes related to lean4#1910, use new notation everywhere (#19369) part 1: make applied occurances of Additive.toAdd and Multiplicative.toMul use newly available dot notation.

Estimated changes

modified theorem toAdd_list_sum
modified theorem toMul_list_sum
modified theorem toMul_multiset_sum
modified theorem toAdd_vadd
modified theorem toMul_smul
modified theorem AddAut.conj_inv_apply
modified theorem even_toAdd_iff
modified theorem isSquare_toMul_iff
modified theorem Int.toAdd_pow
modified theorem Int.toAdd_zpow
modified theorem Nat.toAdd_pow
modified theorem ofAdd_toAdd
modified theorem ofMul_toMul
modified theorem toAdd_div
modified theorem toAdd_inv
modified theorem toAdd_mul
modified theorem toAdd_ofAdd
modified theorem toAdd_one
modified theorem toAdd_pow
modified theorem toAdd_zpow
modified theorem toMul_add
modified theorem toMul_neg
modified theorem toMul_nsmul
modified theorem toMul_ofMul
modified theorem toMul_sub
modified theorem toMul_zero
modified theorem toMul_zsmul
modified theorem Additive.toMul_le
modified theorem Additive.toMul_lt
modified theorem Multiplicative.toAdd_le
modified theorem Multiplicative.toAdd_lt
modified theorem nnnorm_toAdd
modified theorem nnnorm_toMul
modified theorem norm_toAdd
modified theorem norm_toMul
modified theorem zpowersHom_apply
modified theorem zpowersMulHom_apply
modified theorem powersMulHom_apply
modified theorem nhds_toAdd
modified theorem nhds_toMul
modified theorem edist_toAdd
modified theorem edist_toMul
modified theorem dist_toAdd
modified theorem dist_toMul
modified theorem nndist_toAdd
modified theorem nndist_toMul