Theorems · Definition · algebraic geometry
WeierstrassCurve.baseChange
{R : Type u} →
[inst : CommRing R] → WeierstrassCurve R → (A : Type v) → [inst_1 : CommRing A] → [Algebra R A] → WeierstrassCurve AThe Weierstrass curve base changed to an algebra A over R.
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Algebrastatement and proof · cited by 11,388
- Algebra.algebraMapproof · cited by 4,706
- WeierstrassCurvestatement and proof · cited by 394
- WeierstrassCurve.mapproof · cited by 33
Cited by34
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Affine.baseChangeproof · cited by 25
- WeierstrassCurve.Jacobian.baseChangeproof · cited by 21
- WeierstrassCurve.Projective.baseChangeproof · cited by 21
- WeierstrassCurve.map_baseChangestatement · cited by 14
- WeierstrassCurve.baseChange_integralModel_eqstatement · cited by 12
- WeierstrassCurve.integralModel_Δ_eqproof · cited by 2
- WeierstrassCurve.IsIntegral.integralstatement · cited by 2
- WeierstrassCurve.integralModel_c₄_eqproof · cited by 1
- WeierstrassCurve.IsIntegral.casesOnstatement and proof · cited by 1
- WeierstrassCurve.IsIntegral.recOnstatement and proof · cited by 0
- WeierstrassCurve.integralModel_a₂_eqproof · cited by 0
- WeierstrassCurve.baseChange_preΨstatement and proof · cited by 0