English
This ext lemma converts equalities on α^op →+ β into equalities on α →+ β via the opAddEquiv; it is useful for transferring ext results across opposites.
Русский
Это лема экст дает переход от равенств на α^op →+ β к равенствам на α →+ β через opAddEquiv; полезно для переноса экст-результатов через противоположности.
LaTeX
$$$\\text{ext}_{op}$: \\; (f=g)_{α^{op}\\to+β} \\iff (f∘op = g∘op)_{α\\to+β}$$$
Lean4
/-- This ext lemma changes equalities on `αᵐᵒᵖ →+ β` to equalities on `α →+ β`.
This is useful because there are often ext lemmas for specific `α`s that will apply
to an equality of `α →+ β` such as `Finsupp.addHom_ext'`. -/
@[ext]
theorem mul_op_ext {α β} [AddZeroClass α] [AddZeroClass β] (f g : αᵐᵒᵖ →+ β)
(h : f.comp (opAddEquiv : α ≃+ αᵐᵒᵖ).toAddMonoidHom = g.comp (opAddEquiv : α ≃+ αᵐᵒᵖ).toAddMonoidHom) : f = g :=
AddMonoidHom.ext <| MulOpposite.rec' fun x => (DFunLike.congr_fun h :) x
