of_le_right

Mathlib.FieldTheory.LinearDisjoint

URI: https://scilib.ai/kg/mathlib#IntermediateField.LinearDisjoint.of_le_right

← MathLib Explorer

English

If A ⪯ A′ and A is linearly disjoint from L, then A′ is linearly disjoint from L.

Русский

Если A ⊆ A′ и A разобщено с L, то A′ также разобщено с L.

LaTeX

$$$A' \perp_L L$ whenever $A \perp_F L$ and $A' \le A$$$

Lean4

theorem of_le_right {B' : IntermediateField F E} (H : A.LinearDisjoint B) (h : B' ≤ B) : A.LinearDisjoint B' :=
  linearDisjoint_iff'.2 ((linearDisjoint_iff'.1 H).of_le_right_of_flat h)

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

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

Разделы

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

Аффилиация

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