lcm_sup — Mathlib

English

Taking the least common multiple of two orders n1 and n2 yields a cyclotomic extension of order n1.lcm n2 in the ambient field, built from the join of the corresponding subalgebras.

Русский

Наименьшее общее кратное n1 и n2 образует циклотомическое расширение порядка n1.lcm n2, строящееся как сумма (объединение) соответствующих подалгебр.

LaTeX

$$$\\text{IsCyclotomicExtension}(n_1,n_2) \\Rightarrow \\text{IsCyclotomicExtension}(\\operatorname{lcm}(n_1,n_2))$ в соответствующей конструкции$$

Lean4

theorem lcm_sup [NeZero n₁] [NeZero n₂] : IsCyclotomicExtension {n₁.lcm n₂} A (C₁ ⊔ C₂ : Subalgebra A B) :=
  by
  obtain ⟨ζ₁, hζ₁⟩ := h₁.1 rfl (NeZero.ne n₁)
  obtain ⟨ζ₂, hζ₂⟩ := h₂.1 rfl (NeZero.ne n₂)
  replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective C₁ B)
  replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective C₂ B)
  have hζ := hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)
  rw [sup_comm, (isCyclotomicExtension_singleton_iff_eq_adjoin n₁ C₁ hζ₁).mp h₁,
    (isCyclotomicExtension_singleton_iff_eq_adjoin n₂ C₂ hζ₂).mp h₂, ← adjoin_union, Set.union_singleton,
    hζ₁.adjoin_pair_eq A hζ₂ (NeZero.ne _) (NeZero.ne _) hζ]
  have : NeZero (n₁.lcm n₂) := ⟨Nat.lcm_ne_zero (NeZero.ne _) (NeZero.ne _)⟩
  exact (hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)).adjoin_isCyclotomicExtension A

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