Mathlib Map

Theorems · Definition · nonassociative algebras

IsJordan.recOn

{A : Type u_1} →
  [inst : Mul A] →
    {motive : IsJordan A → Sort u} →
      (t : IsJordan A) →
        ((lmul_comm_rmul : ∀ (a b : A), a * b * a = a * (b * a)) →
            (lmul_lmul_comm_lmul : ∀ (a b : A), a * a * (a * b) = a * (a * a * b)) →
              (lmul_lmul_comm_rmul : ∀ (a b : A), a * a * (b * a) = a * a * b * a) →
                (lmul_comm_rmul_rmul : ∀ (a b : A), a * b * (a * a) = a * (b * (a * a))) →
                  (rmul_comm_rmul_rmul : ∀ (a b : A), b * a * (a * a) = b * (a * a) * a) → motive ⋯) →
          motive t
Defined in
Mathlib.Algebra.Jordan.Basic
Cited by
0 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Mul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsJordan · cited by 10IsJordanIsJordan.recOnCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • IsJordanstatement and proof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.