Theorems · Definition · ring theory
Set.star
{α : Type u_1} → [Star α] → Star (Set α)The set (star s : Set α) is defined as {x | star x ∈ s} in the scope Pointwise.
In the usual case where star is involutive, it is equal to {star s | x ∈ s}, see
Set.image_star.
- Defined in
- Mathlib.Algebra.Star.Pointwise
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Star
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.preimageproof · cited by 4,946
- Star.starproof · cited by 1,082
- Starstatement and proof · cited by 496
Cited by30
Results whose statement or proof uses this declaration.
- NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebrastatement · cited by 3
- Set.star_mem_starstatement · cited by 2
- Set.star_subset_starstatement · cited by 1
- Subalgebra.star_adjoin_commstatement · cited by 1
- Set.mem_starstatement · cited by 1
- NonUnitalStarAlgebra.adjoin_eq_spanstatement · cited by 1
- NonUnitalSubalgebra.star_adjoin_commstatement · cited by 1
- Set.nonempty_starstatement · cited by 1
- Set.star_emptystatement · cited by 1
- Set.star_mem_centralizerstatement · cited by 0
- Set.star_mulstatement · cited by 0
- Set.star_preimagestatement · cited by 0