Structures · Algebra
InvolutiveInv
Auxiliary typeclass for types with an involutive Inv.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds inv_inv
Extends1
Extended by1
Concrete types that are instances14
- SeparationQuotient
- ENNReal
- Filter.Germ
- DomMulAct
- Prod
- OrderDual
- MulOpposite
- Lex
- AddOpposite
- Colex
- Multiplicative
- WithZero
- Set
- WithOne
How is a type an instance?
Loading the hierarchy index…
Assumed by124
- inv_inv
- Set.image_inv_eq_inv
- inv_inj
- Equiv.inv
- Homeomorph.inv
- inv_injective
- inv_eq_iff_eq_inv
- Finset.card_inv
- inv_involutive
- Equiv.inv_apply
- inv_mem_iff
- MeasurableEquiv.inv
- Set.inv_singleton
- Set.inv_mem_inv
- tendsto_inv_iff
- inv_surjective
- IsOpen.inv
- Set.inv_subset
- IsCompact.inv
- Set.finite_inv
- MeasureTheory.Measure.inv_inv
- Set.nonempty_inv
- Finset.coe_inv
- MeasureTheory.Measure.inv_apply
- Finset.inv_filter
- IsClosed.inv
- Filter.inv_le_iff_le_inv
- Set.Finite.inv
- inv_coe_set
- inv_closure
- MeasureTheory.lintegral_inv_eq_self
- Set.inv_subset_inv
- Finset.inv_univ
- MeasurableEquiv.inv_apply
- Filter.comap_inv
- Set.inv_range
- Set.Nonempty.inv
- MeasureTheory.Measure.measure_inv
- Cardinal.mk_inv
- isOpenMap_inv
- Submonoid.apply_ne_one_of_mem_or_inv_mem_closure
- IsMulIndecomposable.mem_or_inv_mem_closure_baseOf
- Set.encard_inv
- Set.image_inv_of_apply_inv_eq
- continuousAt_inv_iff
- continuous_inv_iff
- IsMulIndecomposable.image_baseOf_inv_comp_eq
- Set.MapsTo.inv
- Filter.inv_le_inv_iff
- InvolutiveInv.inv_inv