Mathlib Map

Theorems · Theorem · number theory

preNormEDS_two

∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS b c d 2 = 1
Defined in
Mathlib.NumberTheory.EllipticDivisibilitySequence
Cited by
8 results in Mathlib
Foundations
Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

WeierstrassCurve.preΨ_two · cited by 3WeierstrassCurve.preΨ_twopreNormEDS_even · cited by 2preNormEDS_evenpreNormEDS_odd · cited by 2preNormEDS_oddcomplEDS₂_zero · cited by 1complEDS₂_zeronormEDS_two · cited by 1normEDS_twocomplEDS₂_four · cited by 0complEDS₂_fourcomplEDS₂_one · cited by 0complEDS₂_onecomplEDS₂_three · cited by 0complEDS₂_threeCommRing · cited by 17173CommRingmul_one · cited by 3885mul_oneInt.cast_one · cited by 371Int.cast_onepreNormEDS · cited by 25preNormEDSpreNormEDS'_two · cited by 3preNormEDS'_twopreNormEDS_twoCITED BYCITES

Cites5

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

Cited by8

Results whose statement or proof uses this declaration.