instIsIrreducibleFlip — Mathlib

English

If a root pairing P is irreducible, then its flip P.flip is also irreducible.

Русский

Если парение корня P ирредуцируемо, то его отражение P.flip также ирредуцируемо.

LaTeX

$$$$ P.IsIrreducible \Rightarrow P.flip.IsIrreducible. $$$$

Lean4

instance [P.IsIrreducible] : P.flip.IsIrreducible
    where
  nontrivial := IsIrreducible.nontrivial' P
  nontrivial' := IsIrreducible.nontrivial P
  eq_top_of_invtSubmodule_reflection := IsIrreducible.eq_top_of_invtSubmodule_coreflection (P := P)
  eq_top_of_invtSubmodule_coreflection := IsIrreducible.eq_top_of_invtSubmodule_reflection (P := P)

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