primitiveCharacter_isPrimitive — Mathlib

English

The primitiveCharacter χ is primitive: IsPrimitive(primit iveCharacter(χ)).

Русский

Примитивный символ χ является примитивным: IsPrimitive(primitiveCharacter(χ)).

LaTeX

$$$\\operatorname{IsPrimitive}(\\operatorname{primitiveCharacter}(\\chi))$$$

Lean4

theorem primitiveCharacter_isPrimitive : IsPrimitive (χ.primitiveCharacter) :=
  by
  by_cases h : χ.conductor = 0
  · rw [isPrimitive_def]
    convert conductor_eq_zero_iff_level_eq_zero.mpr h
  ·
    exact
      le_antisymm (Nat.le_of_dvd (Nat.pos_of_ne_zero h) (conductor_dvd_level _)) <|
        conductor_le_conductor_mem_conductorSet <| conductor_mem_conductorSet χ

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