normalizedFactors_one — Mathlib

English

normalizedFactors(1) = empty multiset.

Русский

normalizedFactors(1) = пустой мультисет.

LaTeX

$$normalizedFactors(1) = 0$$

Lean4

@[simp]
theorem normalizedFactors_one : normalizedFactors (1 : α) = 0 :=
  by
  rcases subsingleton_or_nontrivial α with h | h
  · dsimp [normalizedFactors, factors]
    simp [Subsingleton.elim (1 : α) 0]
  · rw [← Multiset.rel_zero_right]
    apply factors_unique irreducible_of_normalized_factor
    · intro x hx
      exfalso
      apply Multiset.notMem_zero x hx
    · apply prod_normalizedFactors one_ne_zero

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