Mathlib Map

Theorems · Theorem · number theory

IsEllipticNet.neg_atom

∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b : ℤ), -IsEllipticNet.atom W a b = IsEllipticNet.atom W b a
Defined in
Mathlib.NumberTheory.EllipticDivisibilitySequence
Cited by
3 results in Mathlib
Foundations
Depth 32 from the axioms · uses propext
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsEllipticNet.atom_mul_atom · cited by 1IsEllipticNet.atom_mul_at…IsEllipticNet.atomRel_same₂₄ · cited by 0IsEllipticNet.atomRel_sam…IsEllipticNet.atomRel_same₁₃ · cited by 0IsEllipticNet.atomRel_sam…CommRing · cited by 17173CommRingadd_comm · cited by 1535add_commmul_neg · cited by 590mul_negneg_sub · cited by 272neg_subFunction.Odd · cited by 38Function.OddIsEllipticNet.atom · cited by 25IsEllipticNet.atomIsEllipticNet.neg_atomCITED BYCITES

Cites6

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

Cited by3

Results whose statement or proof uses this declaration.