mono — Mathlib

English

Let m|n and FermatLastTheoremFor m hold; then FermatLastTheoremFor n holds.

Русский

Пусть m делит n и выполняется FermatLastTheoremFor m. Тогда FermatLastTheoremFor n выполняется.

LaTeX

$$$\\forall m,n \\in \\mathbb{N},\\ m \\mid n \\rightarrow (FermatLastTheoremFor\\ m \\rightarrow FermatLastTheoremFor\\ n)$$$

Lean4

theorem mono (hmn : m ∣ n) (hm : FermatLastTheoremFor m) : FermatLastTheoremFor n := by
  exact FermatLastTheoremWith.mono hmn hm

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