English
Conjneg induces a ring homomorphism on the ring of functions, i.e., conjneg preserves addition and multiplication.
Русский
Conjneg задаёт кольцо-оморфизм на кольце функций: conjneg(f+g)=conjneg f+conjneg g и conjneg(f g) = (conjneg f)(conjneg g).
LaTeX
$$$\operatorname{conjneg}(f+g) = \operatorname{conjneg}(f) + \operatorname{conjneg}(g), \quad \operatorname{conjneg}(f\cdot g) = \operatorname{conjneg}(f) \cdot \operatorname{conjneg}(g)$$$
Lean4
/-- `conjneg` bundled as a ring homomorphism. -/
@[simps]
def conjnegRingHom : (G → R) →+* (G → R) where
toFun := conjneg
map_zero' := conjneg_zero
map_one' := conjneg_one
map_add' := conjneg_add
map_mul' := conjneg_mul
