Theorems · Theorem · group theory
Equiv.inv_apply
∀ (G : Type u_14) [inst : InvolutiveInv G], ⇑(Equiv.inv G) = Inv.inv
- Defined in
- Mathlib.Algebra.Group.Equiv.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses Quot.sound
- Assumes
- InvolutiveInv
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.
- DFunLike.coestatement and proof · cited by 62,936
- Equivstatement · cited by 8,337
- InvolutiveInvstatement and proof · cited by 102
- Equiv.invstatement and proof · cited by 23
Cited by11
Results whose statement or proof uses this declaration.
- Matrix.detp_transposeproof · cited by 5
- Matrix.adjp_transposeproof · cited by 2
- Subgroup.normalCore_eq_iInf_comap_conjproof · cited by 1
- Finset.card_div_eqproof · cited by 0
- Matrix.det_eq_detp_sub_detpproof · cited by 0
- ContinuousMultilinearMap.iteratedFDeriv_comp_diagonalproof · cited by 0
- Subgroup.index_dvd_two_iff'proof · cited by 0
- comap_inv_leftUniformSpaceproof · cited by 0
- Set.forall_inv_memproof · cited by 0
- Subgroup.index_eq_two_iff'proof · cited by 0
- Set.exists_inv_memproof · cited by 0