English
Let K be a commutative ring without zero divisors and suppose the group of units K^× is finite. Then the product of all units in K^× equals the negated identity, i.e., ∏_{x ∈ K^×} x = -1 in K^×.
Русский
Пусть K — коммутативное кольцо без делителей нуля и конечна группа единиц K^×. Тогда произведение всех единиц равно -1 в группе единиц: ∏_{u∈K^×} u = -1.
LaTeX
$$$\prod_{x \in K^{\times}} x = -1 \quad \text{in } K^{\times}$$$
Lean4
theorem prod_univ_units_id_eq_neg_one [CommRing K] [IsDomain K] [Fintype Kˣ] : ∏ x : Kˣ, x = (-1 : Kˣ) := by
classical
have : (∏ x ∈ (@univ Kˣ _).erase (-1), x) = 1 :=
prod_involution (fun x _ => x⁻¹) (by simp) (fun a => by simp +contextual [Units.inv_eq_self_iff])
(fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]
