Basic Results about Star on Pi Types #

This file provides basic results about the star on product types defined in Mathlib/Algebra/Notation/Pi/Defs.lean.

instance Pi.instTrivialStarForall {I : Type u} {f : I → Type v} [(i : I) → Star (f i)] [∀ (i : I), TrivialStar (f i)] :

TrivialStar ((i : I) → f i)

@[instance_reducible]

instance Pi.instInvolutiveStarForall {I : Type u} {f : I → Type v} [(i : I) → InvolutiveStar (f i)] :

InvolutiveStar ((i : I) → f i)

Equations

@[instance_reducible]

instance Pi.instStarMulForall {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] [(i : I) → StarMul (f i)] :

StarMul ((i : I) → f i)

Equations

@[instance_reducible]

instance Pi.instStarAddMonoidForall {I : Type u} {f : I → Type v} [(i : I) → AddMonoid (f i)] [(i : I) → StarAddMonoid (f i)] :

StarAddMonoid ((i : I) → f i)

Equations

@[instance_reducible]

instance Pi.instStarRingForall {I : Type u} {f : I → Type v} [(i : I) → NonUnitalSemiring (f i)] [(i : I) → StarRing (f i)] :

StarRing ((i : I) → f i)

Equations

instance Pi.instStarModuleForall {I : Type u} {f : I → Type v} {R : Type w} [(i : I) → SMul R (f i)] [Star R] [(i : I) → Star (f i)] [∀ (i : I), StarModule R (f i)] :

StarModule R ((i : I) → f i)

theorem Pi.single_star {I : Type u} {f : I → Type v} [(i : I) → AddMonoid (f i)] [(i : I) → StarAddMonoid (f i)] [DecidableEq I] (i : I) (a : f i) :

@[simp]

theorem Pi.conj_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CommSemiring (α i)] [(i : ι) → StarRing (α i)] (f : (i : ι) → α i) (i : ι) :

(starRingEnd ((i : ι) → α i)) f i = (starRingEnd (α i)) (f i)

theorem Function.update_star {I : Type u} {f : I → Type v} [(i : I) → Star (f i)] [DecidableEq I] (h : (i : I) → f i) (i : I) (a : f i) :

theorem Function.star_sumElim {I : Type u_1} {J : Type u_2} {α : Type u_3} (x : I → α) (y : J → α) [Star α] :

Documentation