minFac_to_nat — Mathlib

English

For every Num n, the Nat-cast of minFac n equals Nat.minFac n; this reduces to PosNum case via case analysis on n.

Русский

Для каждого числа Num справедливо, что Nat-представление minFac n равно Nat.minFac n; это следует из перехода через случай PosNum.

LaTeX

$$$$\forall n \in \mathrm{Num},\ (\minFac\, n : \mathbb{N}) = \operatorname{Nat}.minFac(n).$$$$

Lean4

@[simp]
theorem minFac_to_nat : ∀ n : Num, (minFac n : ℕ) = Nat.minFac n
  | 0 => rfl
  | pos _ => PosNum.minFac_to_nat _

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