leftDistribClass — Mathlib

English

Ordinal multiplication is left-distributive over addition.

Русский

Умножение ординалов слева распределяется над сложением.

LaTeX

$$LeftDistribClass Ordinal$$

Lean4

instance leftDistribClass : LeftDistribClass Ordinal.{u} :=
  ⟨fun a b c =>
    Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ =>
      Quotient.sound
        ⟨⟨sumProdDistrib _ _ _, by
            rintro ⟨a₁ | a₁, a₂⟩ ⟨b₁ | b₁, b₂⟩ <;>
                simp only [Prod.lex_def, Sum.lex_inl_inl, Sum.Lex.sep, Sum.lex_inr_inl, Sum.lex_inr_inr,
                  sumProdDistrib_apply_left, sumProdDistrib_apply_right, reduceCtorEq] <;>
              simp⟩⟩⟩

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