Mathlib Map

Theorems · Theorem · group theory

Equiv.neg_apply

∀ (G : Type u_14) [inst : InvolutiveNeg G], ⇑(Equiv.neg G) = Neg.neg
Defined in
Mathlib.Algebra.Group.Equiv.Basic
Cited by
34 results in Mathlib
Foundations
Depth 14 from the axioms · uses Quot.sound
Assumes
InvolutiveNeg
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

dvd_neg · cited by 19dvd_negjacobiTheta₂_neg_left · cited by 7jacobiTheta₂_neg_leftjacobiTheta₂'_neg_left · cited by 5jacobiTheta₂'_neg_leftneg_dvd · cited by 3neg_dvdexistsUnique_add_zsmul_mem_Ico · cited by 3existsUnique_add_zsmul_me…existsUnique_sub_zsmul_mem_Ioc · cited by 3existsUnique_sub_zsmul_me…ZMod.LFunction_def_even · cited by 3ZMod.LFunction_def_evenAddSubgroup.index_eq_two_iff' · cited by 2AddSubgroup.index_eq_two_…ZMod.LFunction_def_odd · cited by 2ZMod.LFunction_def_oddFunction.Odd.finsetSum_eq_zero · cited by 2Odd.finsetSum_eq_zeroHasCompactSupport.convolutionExistsAt · cited by 2HasCompactSupport.convolu…Equiv.Perm.sameCycle_inv · cited by 2Perm.sameCycle_invPeriodPair.derivWeierstrassPExcept_neg · cited by 1PeriodPair.derivWeierstra…PeriodPair.derivWeierstrassP_neg · cited by 1PeriodPair.derivWeierstra…AddSubgroup.index_dvd_two_iff' · cited by 1AddSubgroup.index_dvd_two…DFunLike.coe · cited by 62936DFunLike.coeEquiv · cited by 8337EquivInvolutiveNeg · cited by 151InvolutiveNegEquiv.neg · cited by 53Equiv.negEquiv.neg_applyCITED BYCITES

Cites4

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

Cited by34

Results whose statement or proof uses this declaration.