card_nthRoots_subgroup_units — Mathlib

English

The integral closure of a domain inside another domain is a domain.

Русский

Интегральное замыкание области внутри другой области является областью.

LaTeX

$$$IsDomain(integralClosure(R,S))$$$

Lean4

theorem card_nthRoots_subgroup_units [Fintype G] [DecidableEq G] (f : G →* R) (hf : Injective f) {n : ℕ} (hn : 0 < n)
    (g₀ : G) : #{g | g ^ n = g₀} ≤ Multiset.card (nthRoots n (f g₀)) :=
  by
  haveI : DecidableEq R := Classical.decEq _
  calc
    _ ≤ #(nthRoots n (f g₀)).toFinset := card_le_card_of_injOn f (by aesop (add safe unfold Set.MapsTo)) hf.injOn
    _ ≤ _ := (nthRoots n (f g₀)).toFinset_card_le

Похожие утверждения