Theorems · Theorem · group theory
inv_involutive
∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Involutive Inv.inv- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- InvolutiveInv
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- inv_invproof · cited by 494
- Function.Involutivestatement · cited by 103
- InvolutiveInvstatement and proof · cited by 102
Cited by13
Results whose statement or proof uses this declaration.
- Matrix.det_transposeproof · cited by 51
- Set.image_inv_eq_invproof · cited by 44
- Equiv.invproof · cited by 23
- inv_injectiveproof · cited by 17
- inv_eq_iff_eq_invproof · cited by 17
- inv_surjectiveproof · cited by 6
- Set.nonempty_invproof · cited by 3
- Matrix.permanent_transposeproof · cited by 2
- dvd_differentIdeal_of_not_isSeparableproof · cited by 1
- pow_sub_one_dvd_differentIdeal_auxproof · cited by 1
- inv_comp_invproof · cited by 1
- inv_bijectiveproof · cited by 0