mul_left_iff

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsCoprime.mul_left_iff

← MathLib Explorer

English

IsCoprime(x y) z is equivalent to IsCoprime x z and IsCoprime y z.

Русский

IsCoprime(x y) z эквивалентно IsCoprime x z и IsCoprime y z.

LaTeX

$$$IsCoprime(x\cdot y, z) \iff IsCoprime(x,z) \land IsCoprime(y,z)$$$

Lean4

theorem mul_left_iff : IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z :=
  ⟨fun H => ⟨H.of_mul_left_left, H.of_mul_left_right⟩, fun ⟨H1, H2⟩ => H1.mul_left H2⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru