Structures · Algebra
TrivialStar
Typeclass for a trivial star operation. This is mostly meant for ℝ.
- Defined in
- Mathlib.Algebra.Star.Basic
- Shape
- One type argument · adds star_trivial
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances13
- Int
- Nat
- Real
- Rat
- NNReal
- NNRat
- ContinuousMapZero
- MeasureTheory.AEEqFun
- CompactlySupportedContinuousMap
- Subtype
- Prod
- ContinuousMap
- Set
How is a type an instance?
Loading the hierarchy index…
Assumed by93
- conj_trivial
- TrivialStar.star_trivial
- skewAdjointPart
- starL'
- selfAdjointPart
- selfAdjoint.submodule
- skewAdjointPart_apply_coe
- IsSelfAdjoint.all
- selfAdjointPart_apply_coe
- StarModule.decomposeProdAdjoint
- skewAdjoint.submodule
- HasFDerivAtFilter.star
- HasDerivAtFilter.star
- Matrix.conjTransposeAlgEquiv
- Matrix.conjTranspose_eq_transpose_of_trivial
- IsSelfAdjoint.skewAdjointPart_apply
- StarModule.decomposeProdAdjointL
- starL'_apply
- SimpleGraph.posSemidef_lapMatrix
- IsSelfAdjoint.coe_selfAdjointPart_apply
- HasFDerivWithinAt.star
- Matrix.PosDef.of_toQuadraticForm'
- Matrix.PosDef.toQuadraticForm'
- LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix
- selfAdjointPart_comp_subtype_selfAdjoint
- fderiv_star
- deriv.star
- continuous_selfAdjointPart
- fderivWithin_star
- continuous_skewAdjointPart
- Unitary.mem_iff_eq_one_or_eq_neg_one
- selfAdjointPartL
- DifferentiableAt.star
- IsSelfAdjoint.selfAdjointPart_apply
- HasFDerivAt.star
- skewAdjointPartL
- Matrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigen
- DifferentiableWithinAt.star
- Pi.instTrivialStarForall
- isSelfAdjoint_map
- skewAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule
- StarModule.decomposeProdAdjointL_symm_apply
- StarModule.decomposeProdAdjoint_symm_apply
- starL'.congr_simp
- MeasureTheory.AEEqFun.instTrivialStar
- DifferentiableOn.star
- skewAdjointPart_comp_subtype_selfAdjoint
- continuous_decomposeProdAdjoint_symm
- selfAdjoint.instMulActionSubtypeMemAddSubgroupOfStarModule
- selfAdjoint.val_smul
Ancestors0
No ancestors.