Pi

📁 Source: Mathlib/Algebra/Star/Pi.lean

Statistics

Metric	Count
Definitions instInvolutiveStarForall, instStarAddMonoidForall, instStarMulForall, instStarRingForall	4
Theorems star_sumElim, update_star, conj_apply, instStarModuleForall, instTrivialStarForall, single_star	6
Total	10

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
star_sumElim 📖	mathematical	—	Star.star Pi.instStarForall	—	—
update_star 📖	mathematical	—	update Star.star Pi.instStarForall	—	apply_update

Pi

Definitions

Name	Category	Theorems
instInvolutiveStarForall 📖	CompOp	—
instStarAddMonoidForall 📖	CompOp	7 math math: Matrix.intrinsicStar_toLin', intrinsicStar_comul_commSemiring, intrinsicStar_comul, Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff, LinearMap.toMatrix'_intrinsicStar, LinearMap.intrinsicStar_single, LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'
instStarMulForall 📖	CompOp	—
instStarRingForall 📖	CompOp	10 math math: conjneg_conj, cfcₙ_map_pi, CFC.nnrpow_map_pi, CFC.rpow_eq_rpow_pi, CFC.nnrpow_eq_nnrpow_pi, cfc_map_pi, conj_apply, CFC.rpow_map_pi, CFC.sqrt_map_pi, instStarOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike starRingEnd instStarRingForall NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring	—	—
instStarModuleForall 📖	mathematical	StarModule	instStarForall instSMul	—	StarModule.star_smul
instTrivialStarForall 📖	mathematical	TrivialStar	instStarForall	—	TrivialStar.star_trivial
single_star 📖	mathematical	—	single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar instStarForall	—	single_op star_zero

---

← Back to Index