Theorems · Definition · ring theory
selfAdjoint
(R : Type u_1) → [inst : AddGroup R] → [StarAddMonoid R] → AddSubgroup R
The self-adjoint elements of a star additive group, as an additive subgroup.
- Defined in
- Mathlib.Algebra.Star.SelfAdjoint
- Cited by
- 135 results in Mathlib
- Foundations
- Depth 21 from the axioms, rests on 136 definitions · uses propext, Quot.sound
- Assumes
- AddGroupStarAddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- IsSelfAdjointproof · cited by 545
- StarAddMonoidstatement and proof · cited by 296
- IsSelfAdjoint.negproof · cited by 7
Cited by150
Results whose statement or proof uses this declaration.
- realPartstatement · cited by 53
- imaginaryPartstatement · cited by 50
- selfAdjoint.expUnitarystatement and proof · cited by 19
- Unitary.argSelfAdjointstatement · cited by 13
- realPart_add_I_smul_imaginaryPartstatement · cited by 10
- selfAdjointPartstatement · cited by 9
- realPart_apply_coestatement · cited by 9
- selfAdjoint.submoduleproof · cited by 9
- selfAdjoint.expUnitary_coestatement and proof · cited by 8
- imaginaryPart_apply_coestatement · cited by 6
- IsSelfAdjoint.coe_realPartstatement · cited by 6
- selfAdjoint.unitarySelfAddISMulstatement and proof · cited by 6