Commit 2026-11-10 14:10 1d83db4d

View on Github →

feat: use IsApply for OneHom (#45472)

Estimated changes

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

deleted theorem OneHom.div_apply

deleted theorem OneHom.inv_apply

deleted theorem OneHom.mul_apply

added theorem ZeroHom.coe_add

added theorem ZeroHom.coe_neg

added theorem ZeroHom.coe_sub

Modified Mathlib/Algebra/Group/Hom/Defs.lean

deleted theorem OneHom.one_apply

Modified Mathlib/Algebra/Group/Hom/Instances.lean

deleted theorem OneHom.pow_apply

added theorem ZeroHom.nsmul_apply

added theorem ZeroHom.zsmul_apply

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/Factorization/Defs.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

Modified Mathlib/SetTheory/Ordinal/CantorNormalForm.lean