Theorems · Theorem · Lie groups
Circle.star_addChar
∀ {e : AddChar ℝ Circle} (x : ℝ), star ↑(e x) = ↑(e (-x))- Defined in
- Mathlib.Analysis.Complex.Circle
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Submonoidstatement · cited by 3,086
- Star.starstatement · cited by 1,082
- starRingEndproof · cited by 671
- AddCharstatement and proof · cited by 286
- Circlestatement and proof · cited by 227
- Subtype.coe_etaproof · cited by 110
- Submonoid.unitSpherestatement · cited by 85
- AddChar.map_neg_eq_invproof · cited by 9
- Circle.coe_inv_eq_conjproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- BoundedContinuousFunction.char_negproof · cited by 0
- BoundedContinuousFunction.star_mem_range_charAlgHomproof · cited by 0
- Circle.starRingEnd_addCharproof · cited by 0