inf_eq_bot_of_coprime — Mathlib

English

If Nat.card H and Nat.card K are coprime, then H ⊓ K = ⊥.

Русский

Если кардиналы H и K взаимно просты, то их пересечение равно нулевой подгруппе.

LaTeX

$$(Nat.card H).Coprime (Nat.card K) → H ⊓ K = ⊥$$

Lean4

@[to_additive]
theorem inf_eq_bot_of_coprime (h : Nat.Coprime (Nat.card H) (Nat.card K)) : H ⊓ K = ⊥ :=
  card_eq_one.1 <| Nat.eq_one_of_dvd_coprimes h (card_dvd_of_le inf_le_left) (card_dvd_of_le inf_le_right)

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