English
The underlying function of the ring hom constructed from MulSelf data equals the given additive hom f.
Русский
Функция, лежащая в основе кольцевого гомоморфизма, построенного из данных о квадрате, совпадает с данным аддитивным гомоморфизмом f.
LaTeX
$$$(f.mkRingHomOfMulSelfOfTwoNeZero\; h\; h_-two\; h_-one)\!\toFun = f$$
Lean4
/-- Make a ring homomorphism from an additive group homomorphism from a commutative ring to an
integral domain that commutes with self multiplication, assumes that two is nonzero and `1` is sent
to `1`. -/
def mkRingHomOfMulSelfOfTwoNeZero (h : ∀ x, f (x * x) = f x * f x) (h_two : (2 : α) ≠ 0) (h_one : f 1 = 1) : β →+* α :=
{ f with map_one' := h_one,
map_mul' := fun x y => by
have hxy := h (x + y)
rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul, mul_add, mul_add, ←
sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub, ← sub_sub, mul_comm y x,
mul_comm (f y) (f x)] at hxy
simp only [add_assoc, add_sub_assoc, add_sub_cancel] at hxy
rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero (M₀ := α), sub_eq_zero,
or_iff_not_imp_left] at hxy
exact hxy h_two }
