inf_eq_bot — Mathlib

English

If two subfields A and B are linearly disjoint over F, then their intersection is exactly F.

Русский

Если A и B линейно разобщены над F, то их пересечение равно F.

LaTeX

$$$A \cap B = F$ (as subfields of E)$$

Lean4

/-- If `A` and `B` are linearly disjoint over `F`, then their intersection is equal to `F`. -/
theorem inf_eq_bot (H : A.LinearDisjoint B) : A ⊓ B = ⊥ :=
  toSubalgebra_injective (linearDisjoint_iff'.1 H).inf_eq_bot

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