Pointwise

📁 Source: Mathlib/Algebra/Star/Pointwise.lean

Statistics

Metric	Count
Definitions `instInvolutiveStar`	1
Theorems `compl_star`, `iInter_star`, `iUnion_star`, `image_star`, `instTrivialStar`, `inter_star`, `mem_star`, `nonempty_star`, `star_add`, `star_empty`, `star_inv`, `star_inv'`, `star_mem_star`, `star_mul`, `star_preimage`, `star_singleton`, `star_subset`, `star_subset_star`, `star_univ`, `union_star`, `star_coe_eq`	21
Total	22

Set

Definitions

Name	Category	Theorems
`instInvolutiveStar` 📖	CompOp	12 math math: `Module.End.spectrum_intrinsicStar`, `star_centralizer`, `StarMemClass.star_coe_eq`, `NonUnitalStarSubalgebra.coe_centralizer`, `StarSubalgebra.centralizer_toSubalgebra`, `StarAlgebra.star_subset_adjoin`, `StarAlgebra.adjoin_toSubalgebra`, `StarSubalgebra.coe_centralizer_centralizer`, `NonUnitalStarSubalgebra.coe_centralizer_centralizer`, `NonUnitalStarSubalgebra.centralizer_toNonUnitalSubalgebra`, `StarSubalgebra.coe_centralizer`, `StarAlgebra.adjoin_eq_span`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_star` 📖	mathematical	—	`Star.star` `Set` `star` `Compl.compl` `instCompl`	—	`preimage_compl`
`iInter_star` 📖	mathematical	—	`Star.star` `Set` `star` `iInter`	—	`preimage_iInter`
`iUnion_star` 📖	mathematical	—	`Star.star` `Set` `star` `iUnion`	—	`preimage_iUnion`
`image_star` 📖	mathematical	—	`image` `Star.star` `InvolutiveStar.toStar` `Set` `star`	—	`image_eq_preimage_of_inverse` `star_star`
`instTrivialStar` 📖	mathematical	—	`TrivialStar` `Set` `star`	—	`star_preimage` `ext` `TrivialStar.star_trivial`
`inter_star` 📖	mathematical	—	`Star.star` `Set` `star` `instInter`	—	`preimage_inter`
`mem_star` 📖	mathematical	—	`Set` `instMembership` `Star.star` `star`	—	—
`nonempty_star` 📖	mathematical	—	`Nonempty` `Star.star` `Set` `star` `InvolutiveStar.toStar`	—	`Function.Surjective.nonempty_preimage` `Function.Involutive.surjective` `InvolutiveStar.star_involutive`
`star_add` 📖	mathematical	—	`Star.star` `Set` `star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`image_image2` `image2_image_left` `image2_image_right` `image2_congr` `StarAddMonoid.star_add`
`star_empty` 📖	mathematical	—	`Star.star` `Set` `star` `instEmptyCollection`	—	—
`star_inv` 📖	mathematical	—	`Star.star` `Set` `star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext` `star_inv`
`star_inv'` 📖	mathematical	—	`Star.star` `Set` `star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`ext` `star_inv₀`
`star_mem_star` 📖	mathematical	—	`Set` `instMembership` `Star.star` `star` `InvolutiveStar.toStar`	—	`star_star`
`star_mul` 📖	mathematical	—	`Star.star` `Set` `star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `mul`	—	`image_image2` `image2_image_left` `image2_image_right` `image2_congr` `StarMul.star_mul` `image2_swap`
`star_preimage` 📖	mathematical	—	`preimage` `Star.star` `Set` `star`	—	—
`star_singleton` 📖	mathematical	—	`Star.star` `Set` `star` `InvolutiveStar.toStar` `instSingletonSet`	—	`ext` `mem_star` `mem_singleton_iff` `star_eq_iff_star_eq`
`star_subset` 📖	mathematical	—	`Set` `instHasSubset` `Star.star` `star` `InvolutiveStar.toStar`	—	`star_subset_star` `star_star`
`star_subset_star` 📖	mathematical	—	`Set` `instHasSubset` `Star.star` `star` `InvolutiveStar.toStar`	—	`Function.Surjective.preimage_subset_preimage_iff` `Equiv.surjective`
`star_univ` 📖	mathematical	—	`Star.star` `Set` `star` `univ`	—	—
`union_star` 📖	mathematical	—	`Star.star` `Set` `star` `instUnion`	—	`preimage_union`

StarMemClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`star_coe_eq` 📖	mathematical	—	`Star.star` `Set` `InvolutiveStar.toStar` `Set.instInvolutiveStar` `SetLike.coe`	—	`Set.ext` `star_mem_iff`

---

← Back to Index