mul_iff — Mathlib

English

Let p be prime and a,b ∈ α. Then FiniteMultiplicity p (a·b) holds iff FiniteMultiplicity p a and FiniteMultiplicity p b both hold.

Русский

Пусть p — простое. Тогда FiniteMultiplicity p (a·b) эквивално (FiniteMultiplicity p a) и (FiniteMultiplicity p b).

LaTeX

$$$ \forall {a,b} (hp : Prime p), FiniteMultiplicity p (a b) \leftrightarrow (FiniteMultiplicity p a) \land (FiniteMultiplicity p b)$$$

Lean4

theorem mul_iff {p a b : α} (hp : Prime p) :
    FiniteMultiplicity p (a * b) ↔ FiniteMultiplicity p a ∧ FiniteMultiplicity p b :=
  ⟨fun h => ⟨h.mul_left, h.mul_right⟩, fun h => hp.finiteMultiplicity_mul h.1 h.2⟩

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