Mathlib Map

Theorems · Inductive type · group theory

InvolutiveInv

Type u_2 → Type u_2

Auxiliary typeclass for types with an involutive Inv.

Defined in
Mathlib.Algebra.Group.Defs
Cited by
102 results in Mathlib
Foundations
Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

inv_inv · cited by 494inv_invSet.image_inv_eq_inv · cited by 44Set.image_inv_eq_invinv_inj · cited by 25inv_injEquiv.inv · cited by 23Equiv.invHomeomorph.inv · cited by 21Homeomorph.invinv_eq_iff_eq_inv · cited by 17inv_eq_iff_eq_invinv_injective · cited by 17inv_injectiveFinset.card_inv · cited by 14Finset.card_invinv_involutive · cited by 12inv_involutiveinv_mem_iff · cited by 11inv_mem_iffEquiv.inv_apply · cited by 11Equiv.inv_applySet.inv_singleton · cited by 9Set.inv_singletonMeasurableEquiv.inv · cited by 9MeasurableEquiv.invSet.inv_mem_inv · cited by 7Set.inv_mem_invinv_surjective · cited by 6inv_surjectiveInvolutiveInvCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by118

Results whose statement or proof uses this declaration.