Commit 2025-01-10 07:05 220e307b

View on Github →

chore: cleanup more erw (#20601)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/Module/Hom.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

modified def RingEquiv.subsemiringMap

added theorem RingEquiv.subsemiringMap_apply_coe

added theorem RingEquiv.subsemiringMap_symm_apply_coe

Modified Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean