Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+πŸ–±οΈ to focus. On Mac, use ⌘ instead of Ctrl.
Hover-Settings: Show types: Show goals:
import Mathlib.Tactic
import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.Data.Matrix.Notation
import Mathlib.Algebra.Free

-- set_option trace.Meta.synthInstance true
-- set_option synthInstance.checkSynthOrder false


Monoid.mk.{u} {M : Type u} [toSemigroup : Semigroup M] [toOne : One M] (one_mul : βˆ€ (a : M), 1 * a = a)
  (mul_one : βˆ€ (a : M), a * 1 = a) (npow : β„• β†’ M β†’ M) (npow_zero : βˆ€ (x : M), npow 0 x = 1 := by intros; rfl)
  (npow_succ : βˆ€ (n : β„•) (x : M), npow (n + 1) x = npow n x * x := by intros; rfl) : Monoid M
 
Monoid.mk: {M : Type u} β†’
  [toSemigroup : Semigroup M] β†’
    [toOne : One M] β†’
      (βˆ€ (a : M), 1 * a = a) β†’
        (βˆ€ (a : M), a * 1 = a) β†’
          (npow : β„• β†’ M β†’ M) β†’
            autoParam (βˆ€ (x : M), npow 0 x = 1) _auto✝ β†’
              autoParam (βˆ€ (n : β„•) (x : M), npow (n + 1) x = npow n x * x) _auto✝¹ β†’ Monoid M
Monoid.mk


no new constants
 
no new constants
Goals accomplished! πŸ™
 
no new constants
Goals accomplished! πŸ™



AddCommGroup.toIntModule β„€



RingHomClass.mk.{u_5, u_6, u_7} {F : Type u_5} {Ξ± : outParam (Type u_6)} {Ξ² : outParam (Type u_7)} [NonAssocSemiring Ξ±]
  [NonAssocSemiring Ξ²] [FunLike F Ξ± Ξ²] [toMonoidHomClass : MonoidHomClass F Ξ± Ξ²]
  [toAddMonoidHomClass : AddMonoidHomClass F Ξ± Ξ²] : RingHomClass F Ξ± Ξ²
 
RingHomClass.mk: βˆ€ {F : Type u_5} {Ξ± : outParam (Type u_6)} {Ξ² : outParam (Type u_7)} [inst : NonAssocSemiring Ξ±]
  [inst_1 : NonAssocSemiring Ξ²] [inst_2 : FunLike F Ξ± Ξ²] [toMonoidHomClass : MonoidHomClass F Ξ± Ξ²]
  [toAddMonoidHomClass : AddMonoidHomClass F Ξ± Ξ²], RingHomClass F Ξ± Ξ²
RingHomClass.mk -- map_add, map_zero, toMonoidHomClass


MonoidHomClass.mk.{u_10, u_11, u_12} {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)}
  [MulOneClass M] [MulOneClass N] [FunLike F M N] [toMulHomClass : MulHomClass F M N]
  [toOneHomClass : OneHomClass F M N] : MonoidHomClass F M N
 
MonoidHomClass.mk: βˆ€ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : FunLike F M N] [toMulHomClass : MulHomClass F M N] [toOneHomClass : OneHomClass F M N], MonoidHomClass F M N
MonoidHomClass.mk -- map_one, toMulHomClass


MulHomClass.mk.{u_10, u_11, u_12} {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [Mul M] [Mul N]
  [FunLike F M N] (map_mul : βˆ€ (f : F) (x y : M), f (x * y) = f x * f y) : MulHomClass F M N
 
MulHomClass.mk: βˆ€ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : FunLike F M N], (βˆ€ (f : F) (x y : M), f (x * y) = f x * f y) β†’ MulHomClass F M N
MulHomClass.mk -- map_mul, toFunLike


FunLike.{u_1, u_2, u_3} (F : Sort u_1) (Ξ± : Sort u_2) (Ξ² : Sort u_3) : Sort (max (max (max 1 u_1) u_2) u_3)
 
FunLike: Sort u_1 β†’ Sort u_2 β†’ Sort u_3 β†’ Sort (max (max (max 1 u_1) u_2) u_3)
FunLike

-- #check FunLike.mk -- coe, coe_injective'


RingHom.mk.{u_5, u_6} {Ξ± : Type u_5} {Ξ² : Type u_6} [NonAssocSemiring Ξ±] [NonAssocSemiring Ξ²] (toMonoidHom : Ξ± β†’* Ξ²)
  (map_zero' : (↑toMonoidHom).toFun 0 = 0)
  (map_add' : βˆ€ (x y : Ξ±), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y) : Ξ± β†’+* Ξ²
 
RingHom.mk: {Ξ± : Type u_5} β†’
  {Ξ² : Type u_6} β†’
    [inst : NonAssocSemiring Ξ±] β†’
      [inst_1 : NonAssocSemiring Ξ²] β†’
        (toMonoidHom : Ξ± β†’* Ξ²) β†’
          (↑toMonoidHom).toFun 0 = 0 β†’
            (βˆ€ (x y : Ξ±), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y) β†’ Ξ± β†’+* Ξ²
RingHom.mk -- map_zero', map_add', toMonoidHom


MonoidHom.mk.{u_10, u_11} {M : Type u_10} {N : Type u_11} [MulOneClass M] [MulOneClass N] (toOneHom : OneHom M N)
  (map_mul' : βˆ€ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y) : M β†’* N
 
MonoidHom.mk: {M : Type u_10} β†’
  {N : Type u_11} β†’
    [inst : MulOneClass M] β†’
      [inst_1 : MulOneClass N] β†’
        (toOneHom : OneHom M N) β†’ (βˆ€ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y) β†’ M β†’* N
MonoidHom.mk -- map_mul', toOneHom


OneHom.mk.{u_10, u_11} {M : Type u_10} {N : Type u_11} [One M] [One N] (toFun : M β†’ N) (map_one' : toFun 1 = 1) :
  OneHom M N
 
OneHom.mk: {M : Type u_10} β†’ {N : Type u_11} β†’ [inst : One M] β†’ [inst_1 : One N] β†’ (toFun : M β†’ N) β†’ toFun 1 = 1 β†’ OneHom M N
OneHom.mk -- map_one', toFun


Algebra.mk.{u, v} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [toSMul : SMul R A] (toRingHom : R β†’+* A)
  (commutes' : βˆ€ (r : R) (x : A), toRingHom r * x = x * toRingHom r)
  (smul_def' : βˆ€ (r : R) (x : A), r β€’ x = toRingHom r * x) : Algebra R A
 
Algebra.mk: {R : Type u} β†’
  {A : Type v} β†’
    [inst : CommSemiring R] β†’
      [inst_1 : Semiring A] β†’
        [toSMul : SMul R A] β†’
          (toRingHom : R β†’+* A) β†’
            (βˆ€ (r : R) (x : A), toRingHom r * x = x * toRingHom r) β†’
              (βˆ€ (r : R) (x : A), r β€’ x = toRingHom r * x) β†’ Algebra R A
Algebra.mk -- toSMul, toRingHom, commutes', smul_def'


FreeAlgebra.Rel.{u_1, u_2} (R : Type u_1) [CommSemiring R] (X : Type u_2) :
  FreeAlgebra.Pre R X β†’ FreeAlgebra.Pre R X β†’ Prop
 
FreeAlgebra.Rel: (R : Type u_1) β†’ [inst : CommSemiring R] β†’ (X : Type u_2) β†’ FreeAlgebra.Pre R X β†’ FreeAlgebra.Pre R X β†’ Prop
FreeAlgebra.Rel


Warning: declaration uses 'sorry'
 [
CommSemiring: Type u_1 β†’ Type u_1
CommSemiring 
R: Type u_1
R] [
Semiring: Type u_2 β†’ Type u_2
Semiring 
A: Type u_2
A] [
Algebra: (R : Type u_1) β†’ (A : Type u_2) β†’ [inst : CommSemiring R] β†’ [inst : Semiring A] β†’ Type (max u_1 u_2)
Algebra 
R: Type u_1
R 
A: Type u_2
A] (
a: A
a 
b: A
b : 
A: Type u_2
A): 
a: A
a + 
b: A
b = 
b: A
b + 
a: A
a := 
Goals accomplished! πŸ™

  
Warning: 'ring_nf' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
R: Type u_1
A: Type u_2
inst✝²: CommSemiring R
inst✝¹: Semiring A
inst✝: Algebra R A
a, b: A
a + b = b + a

  
Goals accomplished! πŸ™



CliffordAlgebra.ΞΉ.{u_1, u_2} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  (Q : QuadraticForm R M) : M β†’β‚—[R] CliffordAlgebra Q
 
CliffordAlgebra.ΞΉ: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ M β†’β‚—[R] CliffordAlgebra Q
CliffordAlgebra.ΞΉ


CliffordAlgebra.lift.{u_1, u_2, u_3} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  (Q : QuadraticForm R M) {A : Type u_3} [Semiring A] [Algebra R A] :
  { f // βˆ€ (m : M), f m * f m = (algebraMap R A) (Q m) } ≃ (CliffordAlgebra Q →ₐ[R] A)
 
CliffordAlgebra.lift: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’
        [inst_2 : Module R M] β†’
          (Q : QuadraticForm R M) β†’
            {A : Type u_3} β†’
              [inst_3 : Semiring A] β†’
                [inst_4 : Algebra R A] β†’
                  { f // βˆ€ (m : M), f m * f m = (algebraMap R A) (Q m) } ≃ (CliffordAlgebra Q →ₐ[R] A)
CliffordAlgebra.lift


algebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R β†’+* A
 
algebraMap: (R : Type u) β†’ (A : Type v) β†’ [inst : CommSemiring R] β†’ [inst_1 : Semiring A] β†’ [inst_2 : Algebra R A] β†’ R β†’+* A
algebraMap


AlgHom.{u, v, w} (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
  [Algebra R B] : Type (max v w)
 
AlgHom: (R : Type u) β†’
  (A : Type v) β†’
    (B : Type w) β†’
      [inst : CommSemiring R] β†’
        [inst_1 : Semiring A] β†’ [inst_2 : Semiring B] β†’ [inst_3 : Algebra R A] β†’ [inst : Algebra R B] β†’ Type (max v w)
AlgHom


CliffordAlgebra.ΞΉ_comp_lift.{u_1, u_2, u_3} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (f : M β†’β‚—[R] A)
  (cond : βˆ€ (m : M), f m * f m = (algebraMap R A) (Q m)) :
  ((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap βˆ˜β‚— CliffordAlgebra.ΞΉ Q = f
 
CliffordAlgebra.ΞΉ_comp_lift: βˆ€ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M β†’β‚—[R] A)
  (cond : βˆ€ (m : M), f m * f m = (algebraMap R A) (Q m)),
  ((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap βˆ˜β‚— CliffordAlgebra.ΞΉ Q = f
CliffordAlgebra.ΞΉ_comp_lift

-- #check f₁ βˆ˜β‚— fβ‚‚


CliffordAlgebra.lift_unique.{u_1, u_2, u_3} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (f : M β†’β‚—[R] A)
  (cond : βˆ€ (m : M), f m * f m = (algebraMap R A) (Q m)) (g : CliffordAlgebra Q →ₐ[R] A) :
  g.toLinearMap βˆ˜β‚— CliffordAlgebra.ΞΉ Q = f ↔ g = (CliffordAlgebra.lift Q) ⟨f, cond⟩
 
CliffordAlgebra.lift_unique: βˆ€ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M β†’β‚—[R] A)
  (cond : βˆ€ (m : M), f m * f m = (algebraMap R A) (Q m)) (g : CliffordAlgebra Q →ₐ[R] A),
  g.toLinearMap βˆ˜β‚— CliffordAlgebra.ΞΉ Q = f ↔ g = (CliffordAlgebra.lift Q) ⟨f, cond⟩
CliffordAlgebra.lift_unique


ExteriorAlgebra.{u1, u2} (R : Type u1) [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] : Type (max u2 u1)
 
ExteriorAlgebra: (R : Type u1) β†’ [inst : CommRing R] β†’ (M : Type u2) β†’ [inst_1 : AddCommGroup M] β†’ [inst : Module R M] β†’ Type (max u2 u1)
ExteriorAlgebra


TensorAlgebra.toClifford.{u_1, u_2} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M]
  {Q : QuadraticForm R M} : TensorAlgebra R M →ₐ[R] CliffordAlgebra Q
 
TensorAlgebra.toClifford: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’
        [inst_2 : Module R M] β†’ {Q : QuadraticForm R M} β†’ TensorAlgebra R M →ₐ[R] CliffordAlgebra Q
TensorAlgebra.toClifford


Module.Dual.{uR, uM} (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max uM uR)
 
Module.Dual: (R : Type uR) β†’
  (M : Type uM) β†’ [inst : CommSemiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst : Module R M] β†’ Type (max uM uR)
Module.Dual


Module.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
 
Module.Free: (R : Type u) β†’ (M : Type v) β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst : Module R M] β†’ Prop
Module.Free


Module.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
 
Module.Finite: (R : Type u_1) β†’ (M : Type u_4) β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst : Module R M] β†’ Prop
Module.Finite


LinearMap.module.{u_1, u_3, u_5, u_8, u_10} {R : Type u_1} {Rβ‚‚ : Type u_3} {S : Type u_5} {M : Type u_8}
  {Mβ‚‚ : Type u_10} [Semiring R] [Semiring Rβ‚‚] [AddCommMonoid M] [AddCommMonoid Mβ‚‚] [Module R M] [Module Rβ‚‚ Mβ‚‚]
  {σ₁₂ : R β†’+* Rβ‚‚} [Semiring S] [Module S Mβ‚‚] [SMulCommClass Rβ‚‚ S Mβ‚‚] : Module S (M β†’β‚›β‚—[σ₁₂] Mβ‚‚)
 
LinearMap.module: {R : Type u_1} β†’
  {Rβ‚‚ : Type u_3} β†’
    {S : Type u_5} β†’
      {M : Type u_8} β†’
        {Mβ‚‚ : Type u_10} β†’
          [inst : Semiring R] β†’
            [inst_1 : Semiring Rβ‚‚] β†’
              [inst_2 : AddCommMonoid M] β†’
                [inst_3 : AddCommMonoid Mβ‚‚] β†’
                  [inst_4 : Module R M] β†’
                    [inst_5 : Module Rβ‚‚ Mβ‚‚] β†’
                      {σ₁₂ : R β†’+* Rβ‚‚} β†’
                        [inst_6 : Semiring S] β†’
                          [inst_7 : Module S Mβ‚‚] β†’ [inst_8 : SMulCommClass Rβ‚‚ S Mβ‚‚] β†’ Module S (M β†’β‚›β‚—[σ₁₂] Mβ‚‚)
LinearMap.module


Star.star.{u} {R : Type u} [self : Star R] : R β†’ R
 
star: {R : Type u} β†’ [self : Star R] β†’ R β†’ R
star

postfix:max "ᘁ" => 
star: {R : Type u} β†’ [self : Star R] β†’ R β†’ R
star

-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20How.20to.20find.20the.20detailed.20definition.20of.20a.20.22notation.22.20.3F

universe u v
variable (
n2: Type u
n2 : 
Type u: Type (u + 1)
Type u) (
Ξ±2: Type v
Ξ±2 : 
Type v: Type (v + 1)
Type v) [
DivisionMonoid: Type (max v u) β†’ Type (max v u)
DivisionMonoid (
Matrix: Type u β†’ Type u β†’ Type v β†’ Type (max u v)
Matrix 
n2: Type u
n2 
n2: Type u
n2 
Ξ±2: Type v
Ξ±2)] (
A: Matrix n2 n2 Ξ±2
A 
B: Matrix n2 n2 Ξ±2
B : 
Matrix: Type u β†’ Type u β†’ Type v β†’ Type (max u v)
Matrix 
n2: Type u
n2 
n2: Type u
n2 
Ξ±2: Type v
Ξ±2)

/-
[Meta.synthInstance] βœ… HMul (Matrix n2 n2 Ξ±2) (Matrix n2 n2 Ξ±2) (Matrix n2 n2 Ξ±2) β–Ό
  [] new goal HMul (Matrix n2 n2 Ξ±2) (Matrix n2 n2 Ξ±2) _tc.0 β–Ό
    [instances] #[@instHMul, @Matrix.instHMulMatrixMatrixMatrix]
-/

A * B : Matrix n2 n2 Ξ±2
 
A: Matrix n2 n2 Ξ±2
A * 
B: Matrix n2 n2 Ξ±2
B

theorem 
Warning: declaration uses 'sorry'
 : (
A: Matrix n2 n2 Ξ±2
A * 
B: Matrix n2 n2 Ξ±2
B)⁻¹ = 
B: Matrix n2 n2 Ξ±2
B⁻¹ * 
A: Matrix n2 n2 Ξ±2
A⁻¹ := 
Goals accomplished! πŸ™
 
Goals accomplished! πŸ™



Prop : Type
 
Prop: Type
Prop


Bool : Type
 
Bool: Type
Bool

-- TOD: PR

QuadraticMap.associated_left_inverse.{u_1, u_3, u_4} (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R]
  [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] {B₁ : LinearMap.BilinMap R M R}
  (h : LinearMap.IsSymm B₁) : (QuadraticMap.associatedHom S) B₁.toQuadraticMap = B₁
 
QuadraticMap.associated_left_inverse: βˆ€ (S : Type u_1) {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S R] [inst_5 : Invertible 2] {B₁ : LinearMap.BilinMap R M R},
  LinearMap.IsSymm B₁ β†’ (QuadraticMap.associatedHom S) B₁.toQuadraticMap = B₁
QuadraticMap.associated_left_inverse

QuadraticMap.associated_rightInverse.{u_1, u_3, u_4} (S : Type u_1) {R : Type u_3} {M : Type u_4} [CommRing R]
  [AddCommGroup M] [Module R M] [CommSemiring S] [Algebra S R] [Invertible 2] :
  Function.RightInverse (⇑(QuadraticMap.associatedHom S)) LinearMap.BilinMap.toQuadraticMap
 
QuadraticMap.associated_rightInverse: βˆ€ (S : Type u_1) {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S R] [inst_5 : Invertible 2],
  Function.RightInverse (⇑(QuadraticMap.associatedHom S)) LinearMap.BilinMap.toQuadraticMap
QuadraticMap.associated_rightInverse


FreeMagma.rec.{u_1, u} {Ξ± : Type u} {motive : FreeMagma Ξ± β†’ Sort u_1} (of : (a : Ξ±) β†’ motive (FreeMagma.of a))
  (mul : (a a_1 : FreeMagma Ξ±) β†’ motive a β†’ motive a_1 β†’ motive (a.mul a_1)) (t : FreeMagma Ξ±) : motive t
 
FreeMagma.rec: {Ξ± : Type u} β†’
  {motive : FreeMagma Ξ± β†’ Sort u_1} β†’
    ((a : Ξ±) β†’ motive (FreeMagma.of a)) β†’
      ((a a_1 : FreeMagma Ξ±) β†’ motive a β†’ motive a_1 β†’ motive (a.mul a_1)) β†’ (t : FreeMagma Ξ±) β†’ motive t
FreeMagma.rec


FreeMonoid.{u_6} (Ξ± : Type u_6) : Type u_6
 
FreeMonoid: Type u_6 β†’ Type u_6
FreeMonoid


FreeSemigroup.{u} (Ξ± : Type u) : Type u
 
FreeSemigroup: Type u β†’ Type u
FreeSemigroup


FreeRing.{u} (Ξ± : Type u) : Type u
 
FreeRing: Type u β†’ Type u
FreeRing

--#check FreeModule


FreeAlgebra.Rel.{u_1, u_2} (R : Type u_1) [CommSemiring R] (X : Type u_2) :
  FreeAlgebra.Pre R X β†’ FreeAlgebra.Pre R X β†’ Prop
 
FreeAlgebra.Rel: (R : Type u_1) β†’ [inst : CommSemiring R] β†’ (X : Type u_2) β†’ FreeAlgebra.Pre R X β†’ FreeAlgebra.Pre R X β†’ Prop
FreeAlgebra.Rel


example: βˆ€ {Ξ± : Type u_1} {R A : Type} [inst : Monoid Ξ±] (a b : Ξ±), a * b = a * b
example {
Warning: unused variable `R`
note: this linter can be disabled with `set_option linter.unusedVariables false`
 
Warning: unused variable `A`
note: this linter can be disabled with `set_option linter.unusedVariables false`
 : 
Type: Type 1
Type} [
Monoid: Type u_1 β†’ Type u_1
Monoid 
Ξ±: Type u_1
Ξ±] (
a: Ξ±
a 
b: Ξ±
b : 
Ξ±: Type u_1
Ξ±) : 
a: Ξ±
a * 
b: Ξ±
b = 
a: Ξ±
a * 
b: Ξ±
b := 
Goals accomplished! πŸ™
 
Goals accomplished! πŸ™



RingQuot.mk.{uR} {R : Type uR} [Semiring R] {r : R β†’ R β†’ Prop} (toQuot : Quot (RingQuot.Rel r)) : RingQuot r
 
RingQuot.mk: {R : Type uR} β†’ [inst : Semiring R] β†’ {r : R β†’ R β†’ Prop} β†’ Quot (RingQuot.Rel r) β†’ RingQuot r
RingQuot.mk


RingQuot.Rel.{uR} {R : Type uR} [Semiring R] (r : R β†’ R β†’ Prop) : R β†’ R β†’ Prop
 
RingQuot.Rel: {R : Type uR} β†’ [inst : Semiring R] β†’ (R β†’ R β†’ Prop) β†’ R β†’ R β†’ Prop
RingQuot.Rel


Ideal.{u} (R : Type u) [Semiring R] : Type u
 
Ideal: (R : Type u) β†’ [inst : Semiring R] β†’ Type u
Ideal


TensorAlgebra.{u_1, u_2} (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] :
  Type (max u_1 u_2)
 
TensorAlgebra: (R : Type u_1) β†’
  [inst : CommSemiring R] β†’ (M : Type u_2) β†’ [inst_1 : AddCommMonoid M] β†’ [inst : Module R M] β†’ Type (max u_1 u_2)
TensorAlgebra


-- chore(Algebra/FreeAlgebra): fix comments