Theorems · Theorem · number theory
IsEllipticNet.atom_neg_left
∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
Function.Odd W → ∀ (a b : ℤ), IsEllipticNet.atom W (-a) b = IsEllipticNet.atom W a b- Cited by
- 4 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- mul_commproof · cited by 2,262
- neg_subproof · cited by 272
- Function.Oddstatement and proof · cited by 38
- neg_add_eq_subproof · cited by 33
- neg_mul_negproof · cited by 32
- IsEllipticNet.atomstatement and proof · cited by 25
- neg_add'proof · cited by 20
Cited by4
Results whose statement or proof uses this declaration.
- IsEllipticNet.atom_abs_leftproof · cited by 3
- IsEllipticNet.atomRel_neg₁proof · cited by 1
- IsEllipticNet.atomRel_neg₂proof · cited by 1
- IsEllipticNet.atomRel_neg₃proof · cited by 1