def Matrix.KStar.«term𝟙» : Lean.ParserDescr

Equations

• Matrix.KStar.«term𝟙» = Lean.ParserDescr.node `Matrix.KStar.«term𝟙» 1024 (Lean.ParserDescr.symbol "𝟙")

@[implicit_reducible]

instance Matrix.KStar.instKStarUnit_weightedNetKAT {α : Type u_1} [KStar α] : KStar (Matrix Unit Unit α)

Equations

• Matrix.KStar.instKStarUnit_weightedNetKAT = { kstar := fun (m : Matrix Unit Unit α) => KStar.kstar ↑(m () ()) }

instance Matrix.KStar.instLawfulKStarUnit {α : Type u_2} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] : LawfulKStar (Matrix Unit Unit α)

@[implicit_reducible]

noncomputable instance Matrix.KStar.instKStar {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] {n : Type u_2} [Fintype n] [DecidableEq n] : KStar (Matrix n n α)

Equations

• Matrix.KStar.instKStar = { kstar := fun (m : Matrix n n α) => ω∑ (i : ℕ), m ^ i }

instance Matrix.KStar.instLawfulKStar {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] {n : Type u_2} [Fintype n] [DecidableEq n] : LawfulKStar (Matrix n n α)