Theorems · Inductive type · ring theory
StarModule
(R : Type u) → (A : Type v) → [Star R] → [Star A] → [SMul R A] → Prop
A star module A over a star ring R is a module which is a star additive monoid,
and the two star structures are compatible in the sense
star (r • a) = star r • star a.
Note that it is up to the user of this typeclass to enforce
[Semiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A], and that
the statement only requires [Star R] [Star A] [SMul R A].
If used as [CommRing R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A], this represents a
star algebra.
- Defined in
- Mathlib.Algebra.Star.Basic
- Cited by
- 570 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Starstatement · cited by 496
Cited by661
Results whose statement or proof uses this declaration.
- StarSubalgebrastatement · cited by 194
- StarSubalgebra.toSubalgebrastatement and proof · cited by 58
- realPartstatement and proof · cited by 53
- imaginaryPartstatement and proof · cited by 50
- NonUnitalStarAlgebra.adjoinstatement and proof · cited by 43
- StarAlgebra.adjoinstatement and proof · cited by 42
- StarModule.star_smulstatement and proof · cited by 34
- StarAlgebra.elementalstatement and proof · cited by 26
- StarSubalgebra.mapstatement and proof · cited by 24
- StarSubalgebra.topologicalClosurestatement and proof · cited by 22
- selfAdjoint.expUnitarystatement and proof · cited by 19
- NonUnitalStarAlgebra.elementalstatement and proof · cited by 19
Showing the 200 most cited of 661.