embedding

Mathlib.RingTheory.Idempotents

URI: https://scilib.ai/kg/mathlib#OrthogonalIdempotents.embedding

English

For any embedding i: J ↪ I, OrthogonalIdempotents (e ∘ i) holds.

Русский

Для любого вложения i: J ↪ I выполняется OrthogonalIdempotents (e ∘ i).

LaTeX

$$OrthogonalIdempotents (e ∘ i)$$

Lean4

theorem embedding (he : OrthogonalIdempotents e) {J} (i : J ↪ I) : OrthogonalIdempotents (e ∘ i) := by
  classical simp [iff_mul_eq, he.mul_eq]

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

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

Разделы

Аффилиация

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