Weierstrass

📁 Source: Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

Statistics

Metric	Count
Definitions WeierstrassCurve, IsElliptic, a₁, a₂, a₃, a₄, a₆, baseChange, b₂, b₄, b₆, b₈, c₄, c₆, instInhabited, j, map, twoTorsionPolynomial, Δ, Δ'	20
Theorems isUnit, b_relation, b_relation_of_char_three, b_relation_of_char_two, b₂_of_char_three, b₂_of_char_two, b₄_of_char_three, b₄_of_char_two, b₆_of_char_three, b₆_of_char_two, b₈_of_char_three, b₈_of_char_two, c_relation, c_relation_of_char_three, c_relation_of_char_two, coe_inv_map_Δ', coe_map_Δ', coe_Δ', c₄_of_char_three, c₄_of_char_two, c₆_of_char_three, c₆_of_char_two, ext, ext_iff, instIsEllipticMap, inv_map_Δ', isElliptic_iff, isUnit_Δ, j_eq_zero, j_eq_zero_iff, j_eq_zero_iff', j_eq_zero_iff_of_char_three, j_eq_zero_iff_of_char_three', j_eq_zero_iff_of_char_two, j_eq_zero_iff_of_char_two', j_eq_zero_of_char_three, j_eq_zero_of_char_two, j_of_char_three, j_of_char_two, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆, map_baseChange, map_b₂, map_b₄, map_b₆, map_b₈, map_c₄, map_c₆, map_id, map_injective, map_j, map_map, map_Δ, map_Δ', twoTorsionPolynomial_disc, twoTorsionPolynomial_disc_isUnit, twoTorsionPolynomial_disc_ne_zero, twoTorsionPolynomial_disc_ne_zero_of_isElliptic, twoTorsionPolynomial_disc_of_char_three, twoTorsionPolynomial_disc_of_char_two, twoTorsionPolynomial_discr, twoTorsionPolynomial_discr_isUnit, twoTorsionPolynomial_discr_ne_zero, twoTorsionPolynomial_discr_ne_zero_of_isElliptic, twoTorsionPolynomial_discr_of_char_three, twoTorsionPolynomial_discr_of_char_two, twoTorsionPolynomial_of_char_three, twoTorsionPolynomial_of_char_two, Δ_of_char_three, Δ_of_char_two	73
Total	93

WeierstrassCurve

Definitions

Name	Category	Theorems
IsElliptic 📖	CompData	8 math math: instIsEllipticOfJ0OfFactIsUnitOfNat, instIsEllipticHSMulVariableChange, instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat, instIsEllipticOfJ1728OfFactIsUnitOfNat, instIsEllipticMap, isElliptic_iff, isGoodReduction_iff_isElliptic_reduction, instIsEllipticOfJ
a₁ 📖	CompOp	77 math math: b₂_of_char_three, j_of_char_two, Projective.eval_polynomial, Projective.negY_eq, b₈_of_char_two, variableChange_a₁, isCharTwoJNeZeroNF_iff, Jacobian.eval_polynomialY, Jacobian.negY_eq, Projective.dblU_eq, b₂_of_char_two, Affine.equation_iff', Affine.polynomial_eq, a₁_of_isShortNF, Jacobian.polynomialY_eq, Jacobian.eval_polynomialX, a₁_of_isCharTwoJNeZeroNF, Projective.eval_polynomialX, toCharNeTwoNF_s, Projective.negAddY_eq', Affine.slope_of_Y_ne, b₄_of_char_three, Projective.polynomialZ_eq, a₁_of_isCharNeTwoNF, Jacobian.addX_eq', isCharThreeJNeZeroNF_iff, Affine.CoordinateRing.norm_smul_basis, isCharNeTwoNF_iff, variableChange_def, Affine.addPolynomial_eq, variableChange_a₂, variableChange_a₃, Projective.eval_polynomialZ, Projective.polynomialX_eq, Projective.polynomialY_eq, Projective.negDblY_eq, Projective.addX_eq, variableChange_a₄, a₁_of_isCharTwoJEqZeroNF, ext_iff, Jacobian.polynomialZ_eq, Jacobian.dblU_eq, isCharTwoJEqZeroNF_iff, b₄_of_char_two, Jacobian.equation_iff, Projective.negDblY_eq', Affine.equation_iff, isShortNF_iff, Projective.negAddY_eq, Jacobian.addX_eq, b₈_of_char_three, Affine.evalEval_polynomialY, Jacobian.eval_polynomial, IsCharThreeJNeZeroNF.a₁, Projective.addX_eq', Affine.CoordinateRing.coe_norm_smul_basis, j_eq_zero_iff_of_char_two', Jacobian.polynomialX_eq, c₆_of_char_two, Affine.evalEval_polynomial, Affine.evalEval_polynomialX, IsCharTwoJEqZeroNF.a₁, Projective.dblX_eq, map_a₁, j_eq_zero_iff_of_char_two, a₁_of_isCharThreeJNeZeroNF, Projective.equation_iff, IsCharTwoJNeZeroNF.a₁, Projective.dblX_eq', IsCharNeTwoNF.a₁, variableChange_a₆, Projective.eval_polynomialY, Jacobian.eval_polynomialZ, IsShortNF.a₁, Affine.CoordinateRing.smul_basis_mul_Y, Δ_of_char_two, c₄_of_char_two
a₂ 📖	CompOp	68 math math: b₂_of_char_three, map_a₂, c₆_of_isCharThreeJNeZeroNF_of_char_three, Projective.eval_polynomial, b₈_of_char_two, b₂_of_isCharThreeJNeZeroNF, b₈_of_isCharNeTwoNF, Projective.dblU_eq, Affine.equation_iff', Affine.polynomial_eq, b₂_of_isCharTwoJNeZeroNF, b₂_of_isCharNeTwoNF, Jacobian.eval_polynomialX, c₆_of_isCharThreeJNeZeroNF, Projective.eval_polynomialX, Projective.negAddY_eq', Affine.slope_of_Y_ne, c₄_of_isCharThreeJNeZeroNF, Affine.slope_of_Y_ne', IsShortNF.a₂, Projective.polynomialZ_eq, Jacobian.addX_eq', Affine.CoordinateRing.norm_smul_basis, variableChange_def, Affine.addPolynomial_eq, variableChange_a₂, Projective.eval_polynomialZ, Projective.polynomialX_eq, b₈_of_isCharThreeJNeZeroNF, Projective.negDblY_eq, Projective.addX_eq, variableChange_a₄, c₆_of_isCharNeTwoNF, ext_iff, Jacobian.polynomialZ_eq, Jacobian.dblU_eq, isCharTwoJEqZeroNF_iff, Δ_of_isCharNeTwoNF, Jacobian.equation_iff, Projective.negDblY_eq', Affine.equation_iff, isShortNF_iff, Projective.negAddY_eq, toShortNFOfCharThree_a₂, Jacobian.addX_eq, b₈_of_char_three, Jacobian.eval_polynomial, Projective.addX_eq', c₄_of_isCharNeTwoNF, Jacobian.polynomialX_eq, Affine.evalEval_polynomial, b₂_of_isCharThreeJNeZeroNF_of_char_three, Affine.evalEval_polynomialX, Δ_of_isCharThreeJNeZeroNF, Projective.dblX_eq, Projective.equation_iff, a₂_of_isShortNF, Projective.dblX_eq', c₄_of_isCharThreeJNeZeroNF_of_char_three, Δ_of_isCharThreeJNeZeroNF_of_char_three, a₂_of_isCharTwoJEqZeroNF, variableChange_a₆, Jacobian.eval_polynomialZ, b₈_of_isCharThreeJNeZeroNF_of_char_three, j_of_isCharThreeJNeZeroNF_of_char_three, Affine.CoordinateRing.smul_basis_mul_Y, IsCharTwoJEqZeroNF.a₂, b₈_of_isCharTwoJNeZeroNF
a₃ 📖	CompOp	51 math math: Projective.eval_polynomial, toCharNeTwoNF_t, Projective.negY_eq, b₈_of_char_two, isCharTwoJNeZeroNF_iff, Jacobian.eval_polynomialY, IsCharTwoJNeZeroNF.a₃, Jacobian.negY_eq, a₃_of_isCharThreeJNeZeroNF, Affine.equation_iff', Affine.polynomial_eq, b₆_of_char_three, Jacobian.polynomialY_eq, b₄_of_char_three, Projective.polynomialZ_eq, isCharThreeJNeZeroNF_iff, Affine.CoordinateRing.norm_smul_basis, isCharNeTwoNF_iff, variableChange_def, Affine.addPolynomial_eq, variableChange_a₃, Projective.eval_polynomialZ, IsShortNF.a₃, a₃_of_isCharNeTwoNF, Projective.polynomialY_eq, variableChange_a₄, ext_iff, Jacobian.polynomialZ_eq, b₄_of_char_two, Affine.evalEval_polynomialY_zero, Jacobian.equation_iff, Affine.equation_iff, isShortNF_iff, Δ_of_isCharTwoJEqZeroNF_of_char_two, b₈_of_char_three, Affine.evalEval_polynomialY, Jacobian.eval_polynomial, Affine.CoordinateRing.coe_norm_smul_basis, Affine.evalEval_polynomial, IsCharNeTwoNF.a₃, a₃_of_isShortNF, map_a₃, IsCharThreeJNeZeroNF.a₃, b₆_of_char_two, Projective.equation_iff, variableChange_a₆, Projective.eval_polynomialY, Jacobian.eval_polynomialZ, Affine.CoordinateRing.smul_basis_mul_Y, Δ_of_char_two, a₃_of_isCharTwoJNeZeroNF
a₄ 📖	CompOp	57 math math: Projective.eval_polynomial, b₈_of_char_two, Δ_of_isCharTwoJEqZeroNF, isCharTwoJNeZeroNF_iff, b₈_of_isCharNeTwoNF, Projective.dblU_eq, Affine.equation_iff', Affine.polynomial_eq, b₈_of_isCharTwoJEqZeroNF_of_char_two, b₄_of_isShortNF_of_char_three, b₈_of_isCharTwoJEqZeroNF, Jacobian.eval_polynomialX, Projective.eval_polynomialX, Affine.slope_of_Y_ne, Affine.slope_of_Y_ne', b₄_of_char_three, Projective.polynomialZ_eq, map_a₄, Δ_of_isShortNF, isCharThreeJNeZeroNF_iff, Affine.CoordinateRing.norm_smul_basis, a₄_of_isCharThreeJNeZeroNF, Δ_of_isShortNF_of_char_three, variableChange_def, Affine.addPolynomial_eq, Projective.eval_polynomialZ, b₄_of_isShortNF, Projective.polynomialX_eq, c₄_of_isShortNF, variableChange_a₄, c₆_of_isCharNeTwoNF, ext_iff, j_of_isCharTwoJEqZeroNF, Jacobian.polynomialZ_eq, Jacobian.dblU_eq, Δ_of_isCharNeTwoNF, Jacobian.equation_iff, Affine.equation_iff, IsCharThreeJNeZeroNF.a₄, b₈_of_char_three, Jacobian.eval_polynomial, IsCharTwoJNeZeroNF.a₄, c₄_of_isCharNeTwoNF, Jacobian.polynomialX_eq, Affine.evalEval_polynomial, Affine.evalEval_polynomialX, c₄_of_isCharTwoJEqZeroNF, b₄_of_isCharNeTwoNF, b₈_of_isShortNF, Projective.equation_iff, j_of_isShortNF, b₄_of_isCharTwoJEqZeroNF, a₄_of_isCharTwoJNeZeroNF, variableChange_a₆, Affine.evalEval_polynomialX_zero, Jacobian.eval_polynomialZ, Affine.CoordinateRing.smul_basis_mul_Y
a₆ 📖	CompOp	48 math math: Projective.eval_polynomial, b₈_of_char_two, b₈_of_isCharNeTwoNF, Affine.equation_iff', Affine.polynomial_eq, Affine.nonsingular_zero, b₆_of_char_three, c₆_of_isCharThreeJNeZeroNF, b₈_of_isCharTwoJNeZeroNF_of_char_two, b₆_of_isCharTwoJNeZeroNF, Projective.polynomialZ_eq, Δ_of_isShortNF, b₆_of_isShortNF, map_a₆, Affine.CoordinateRing.norm_smul_basis, b₆_of_isCharThreeJNeZeroNF, variableChange_def, Affine.addPolynomial_eq, Projective.eval_polynomialZ, Affine.evalEval_polynomial_zero, Affine.equation_zero, c₆_of_isCharTwoJNeZeroNF, b₈_of_isCharThreeJNeZeroNF, b₆_of_isCharThreeJNeZeroNF_of_char_three, c₆_of_isCharNeTwoNF, ext_iff, Jacobian.polynomialZ_eq, b₆_of_isShortNF_of_char_three, Δ_of_isCharNeTwoNF, Jacobian.equation_iff, Affine.equation_iff, b₈_of_char_three, Jacobian.eval_polynomial, b₆_of_isCharNeTwoNF, Affine.evalEval_polynomial, Δ_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharThreeJNeZeroNF, Projective.equation_iff, j_of_isShortNF, Δ_of_isCharThreeJNeZeroNF_of_char_three, c₆_of_isShortNF, variableChange_a₆, j_of_isCharTwoJNeZeroNF_of_char_two, Jacobian.eval_polynomialZ, b₈_of_isCharThreeJNeZeroNF_of_char_three, j_of_isCharThreeJNeZeroNF_of_char_three, Affine.CoordinateRing.smul_basis_mul_Y, b₈_of_isCharTwoJNeZeroNF
baseChange 📖	CompOp	68 math math: baseChange_ΨSq, Affine.baseChange_nonsingular, Projective.baseChange_negDblY, baseChange_preΨ, Jacobian.baseChange_polynomialZ, baseChange_preΨ₄, Projective.baseChange_negAddY, Projective.baseChange_negY, baseChange_Ψ₂Sq, baseChange_preΨ', Affine.baseChange_negY, baseChange_ψ₂, Projective.baseChange_polynomial, Affine.baseChange_negPolynomial, Projective.baseChange_dblXYZ, Jacobian.baseChange_nonsingular, Jacobian.baseChange_addX, Jacobian.baseChange_equation, Projective.baseChange_addXYZ, Jacobian.baseChange_addXYZ, baseChange_φ, Affine.Point.map_injective, Jacobian.baseChange_dblX, Jacobian.baseChange_negDblY, Jacobian.baseChange_polynomialY, Projective.baseChange_polynomialY, Jacobian.baseChange_dblY, baseChange_integralModel_eq, baseChange_Φ, Projective.baseChange_equation, Jacobian.baseChange_dblU, Jacobian.baseChange_polynomial, Affine.Point.map_baseChange, Projective.baseChange_dblZ, Affine.baseChange_addPolynomial, baseChange_Ψ, Projective.baseChange_polynomialX, Affine.baseChange_polynomialX, Jacobian.baseChange_neg, Affine.Point.map_map, map_baseChange, Affine.baseChange_equation, Affine.baseChange_polynomial, Jacobian.baseChange_dblXYZ, baseChange_ψ, Projective.baseChange_addX, Jacobian.baseChange_dblZ, Jacobian.baseChange_polynomialX, Projective.baseChange_dblX, Projective.baseChange_dblU, Projective.baseChange_nonsingular, Affine.baseChange_slope, Affine.baseChange_addY, Projective.baseChange_neg, IsIntegral.integral, Projective.baseChange_polynomialZ, Affine.baseChange_polynomialY, Affine.baseChange_addX, Jacobian.baseChange_negY, Affine.Point.map_zero, Projective.baseChange_dblY, isIntegral_iff, Projective.baseChange_addY, Jacobian.baseChange_addY, Affine.baseChange_negAddY, baseChange_Ψ₃, Jacobian.baseChange_negAddY, Affine.Point.map_id
b₂ 📖	CompOp	28 math math: b₂_of_char_three, c₄_of_char_three, b_relation_of_char_two, b₂_of_isCharThreeJNeZeroNF, j_of_char_three, b₂_of_char_two, b₂_of_isCharTwoJNeZeroNF, b₂_of_isCharNeTwoNF, variableChange_b₈, Δ_of_char_three, variableChange_b₂, variableChange_b₆, c₄_of_isCharTwoJNeZeroNF, b₂_of_isShortNF, c₆_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two, b_relation_of_char_three, b_relation, toShortNFOfCharThree_a₂, twoTorsionPolynomial_of_char_three, b₂_of_isCharThreeJNeZeroNF_of_char_three, j_eq_zero_iff_of_char_three, c₆_of_char_three, twoTorsionPolynomial_of_char_two, j_eq_zero_iff_of_char_three', map_b₂, b₂_of_isCharTwoJEqZeroNF, variableChange_b₄
b₄ 📖	CompOp	19 math math: b_relation_of_char_two, b₄_of_isShortNF_of_char_three, variableChange_b₈, Δ_of_char_three, b₄_of_char_three, variableChange_b₆, b₄_of_isShortNF, b₄_of_isCharThreeJNeZeroNF, b₄_of_char_two, b_relation_of_char_three, b_relation, Φ_two, twoTorsionPolynomial_of_char_three, b₄_of_isCharTwoJNeZeroNF, map_b₄, b₄_of_isCharNeTwoNF, b₄_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF_of_char_two, variableChange_b₄
b₆ 📖	CompOp	21 math math: Δ_of_isCharTwoJEqZeroNF, b_relation_of_char_two, b₆_of_char_three, b₆_of_isCharTwoJNeZeroNF_of_char_two, variableChange_b₈, b₆_of_isCharTwoJNeZeroNF, variableChange_b₆, b₆_of_isShortNF, map_b₆, b₆_of_isCharThreeJNeZeroNF, c₆_of_isCharTwoJEqZeroNF, b₆_of_isCharThreeJNeZeroNF_of_char_three, j_of_isCharTwoJEqZeroNF, b₆_of_isShortNF_of_char_three, b_relation_of_char_three, b_relation, Φ_two, twoTorsionPolynomial_of_char_three, b₆_of_isCharNeTwoNF, twoTorsionPolynomial_of_char_two, b₆_of_char_two
b₈ 📖	CompOp	17 math math: b₈_of_char_two, b₈_of_isCharNeTwoNF, b₈_of_isCharTwoJEqZeroNF_of_char_two, b₈_of_isCharTwoJEqZeroNF, variableChange_b₈, b₈_of_isCharTwoJNeZeroNF_of_char_two, map_b₈, Δ_of_char_three, b₈_of_isCharThreeJNeZeroNF, b_relation_of_char_three, b_relation, Φ_two, b₈_of_char_three, b₈_of_isShortNF, b₈_of_isCharThreeJNeZeroNF_of_char_three, Δ_of_char_two, b₈_of_isCharTwoJNeZeroNF
c₄ 📖	CompOp	21 math math: c₄_of_char_three, c_relation, ofJNe0Or1728_c₄, c₄_of_isCharThreeJNeZeroNF, j_eq_zero_iff', c₄_of_isCharTwoJNeZeroNF, ofJ0_c₄, c₄_of_isShortNF, c₄_of_isShortNF_of_char_three, c₄_of_isCharNeTwoNF, map_c₄, c₄_of_isCharTwoJEqZeroNF_of_char_two, c₄_of_isCharTwoJEqZeroNF, c₄_of_isCharThreeJNeZeroNF_of_char_three, variableChange_c₄, c₄_of_isCharTwoJNeZeroNF_of_char_two, j_eq_zero_iff, c_relation_of_char_three, c₄_of_char_two, ofJ1728_c₄, c_relation_of_char_two
c₆ 📖	CompOp	16 math math: c₆_of_isCharThreeJNeZeroNF_of_char_three, c_relation, map_c₆, c₆_of_isCharThreeJNeZeroNF, variableChange_c₆, c₆_of_isCharTwoJEqZeroNF, c₆_of_isCharTwoJNeZeroNF, c₆_of_isCharTwoJEqZeroNF_of_char_two, c₆_of_isCharNeTwoNF, c₆_of_char_two, c₆_of_char_three, c₆_of_isShortNF, c₆_of_isShortNF_of_char_three, c_relation_of_char_three, c₆_of_isCharTwoJNeZeroNF_of_char_two, c_relation_of_char_two
instInhabited 📖	CompOp	—
j 📖	CompOp	23 math math: j_of_char_two, variableChange_j, ofJ_j, j_of_char_three, j_eq_zero_iff', j_of_isCharTwoJEqZeroNF_of_char_two, j_eq_zero, ofJ1728_j, j_of_isCharTwoJEqZeroNF, ofJ0_j, j_eq_zero_of_char_three, j_eq_zero_iff_of_char_two', ofJNe0Or1728_j, j_eq_zero_iff_of_char_three, j_of_isShortNF_of_char_three, j_eq_zero_iff_of_char_two, j_eq_zero_iff_of_char_three', j_of_isShortNF, map_j, j_eq_zero_of_char_two, j_of_isCharTwoJNeZeroNF_of_char_two, j_eq_zero_iff, j_of_isCharThreeJNeZeroNF_of_char_three
map 📖	CompOp	91 math math: Jacobian.map_addX, Projective.map_dblZ, map_ψ₂, Projective.map_neg, map_a₂, map_Ψ₂Sq, map_φ, Jacobian.map_equation, Jacobian.map_dblX, map_Ψ, Jacobian.map_negDblY, Projective.map_negAddY, Affine.map_polynomialY, map_c₆, Affine.map_addY, map_id, Jacobian.map_negY, Jacobian.map_dblZ, coe_map_Δ', map_b₈, Projective.map_negDblY, map_a₄, Jacobian.map_add, Affine.map_negPolynomial, map_injective, map_a₆, map_b₆, Jacobian.map_dblXYZ, Jacobian.map_addY, Affine.map_slope, Projective.map_polynomialX, Affine.CoordinateRing.map_mk, map_Φ, map_preΨ', Projective.map_addY, Projective.map_dblY, Jacobian.map_nonsingular, Projective.map_dblU, Affine.map_polynomial, coe_inv_map_Δ', map_ΨSq, map_variableChange, map_baseChange, Affine.map_nonsingular, Affine.CoordinateRing.map_injective, Affine.map_negAddY, Projective.map_equation, Affine.map_equation, instIsEllipticMap, Jacobian.map_polynomialZ, Projective.map_addXYZ, Projective.map_polynomialZ, Jacobian.Equation.map, map_preΨ, map_Ψ₃, Projective.map_dblXYZ, Jacobian.map_negAddY, Jacobian.map_polynomial, map_c₄, Affine.map_polynomialX, map_preΨ₄, map_b₄, Jacobian.map_dblY, Projective.map_addX, Projective.map_addZ, map_Δ', Jacobian.map_dblU, Projective.Equation.map, Affine.Equation.map, Projective.map_add, inv_map_Δ', Affine.map_addPolynomial, map_a₃, map_a₁, Affine.map_negY, map_ψ, map_j, Jacobian.map_polynomialY, Affine.CoordinateRing.map_smul, map_Δ, Affine.map_addX, Projective.map_polynomialY, Projective.map_polynomial, Projective.map_nonsingular, Projective.map_negY, map_b₂, Jacobian.map_polynomialX, Jacobian.map_neg, map_map, Jacobian.map_addXYZ, Projective.map_dblX
twoTorsionPolynomial 📖	CompOp	11 math math: twoTorsionPolynomial_discr_of_char_three, twoTorsionPolynomial_disc_of_char_three, twoTorsionPolynomial_disc_of_char_two, Ψ₂Sq_eq, twoTorsionPolynomial_discr_isUnit, twoTorsionPolynomial_disc_isUnit, twoTorsionPolynomial_of_char_three, twoTorsionPolynomial_disc, twoTorsionPolynomial_discr_of_char_two, twoTorsionPolynomial_of_char_two, twoTorsionPolynomial_discr
Δ 📖	CompOp	31 math math: c_relation, twoTorsionPolynomial_discr_of_char_three, ofJNe0Or1728_Δ, twoTorsionPolynomial_disc_of_char_three, Δ_of_isCharTwoJEqZeroNF, valuation_Δ_aux_eq_of_isIntegral, integralModel_Δ_eq, IsElliptic.isUnit, ofJ0_Δ, Δ_of_char_three, Δ_of_isShortNF, isGoodReduction_iff, Δ_of_isShortNF_of_char_three, twoTorsionPolynomial_discr_isUnit, variableChange_Δ, twoTorsionPolynomial_disc_isUnit, Δ_integral_of_isIntegral, isUnit_Δ, Δ_of_isCharNeTwoNF, coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, twoTorsionPolynomial_disc, Δ_of_isCharTwoJNeZeroNF_of_char_two, isElliptic_iff, Δ_of_isCharThreeJNeZeroNF, twoTorsionPolynomial_discr, IsGoodReduction.goodReduction, map_Δ, Δ_of_isCharThreeJNeZeroNF_of_char_three, ofJ1728_Δ, Δ_of_char_two
Δ' 📖	CompOp	11 math math: j_of_char_two, variableChange_Δ', j_of_char_three, coe_map_Δ', coe_inv_variableChange_Δ', inv_variableChange_Δ', coe_inv_map_Δ', coe_Δ', coe_variableChange_Δ', map_Δ', inv_map_Δ'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
b_relation 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat b₈ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup b₂ b₆ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b₄	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
b_relation_of_char_three 📖	mathematical	—	b₈ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing b₂ b₆ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b₄	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq b_relation Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
b_relation_of_char_two 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing b₂ b₆ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b₄	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq b_relation Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
b₂_of_char_three 📖	mathematical	—	b₂ Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁ a₂	—	b₂.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
b₂_of_char_two 📖	mathematical	—	b₂ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁	—	b₂.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
b₄_of_char_three 📖	mathematical	—	b₄ Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing a₄ Distrib.toMul a₁ a₃	—	b₄.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
b₄_of_char_two 📖	mathematical	—	b₄ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing a₁ a₃	—	b₄.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
b₆_of_char_three 📖	mathematical	—	b₆ Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₃ a₆	—	b₆.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
b₆_of_char_two 📖	mathematical	—	b₆ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₃	—	b₆.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
b₈_of_char_three 📖	mathematical	—	b₈ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁ a₆ a₂ a₃ a₄	—	b₈.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
b₈_of_char_two 📖	mathematical	—	b₈ Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁ a₆ a₃ a₄ a₂	—	b₈.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
c_relation 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Δ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring c₄ c₆	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
c_relation_of_char_three 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring c₄ c₆	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq c_relation Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
c_relation_of_char_two 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring c₄ c₆	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq c_relation Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
coe_inv_map_Δ' 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv Δ' map instIsEllipticMap DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	instIsEllipticMap MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_Δ'
coe_map_Δ' 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Δ' map instIsEllipticMap DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	instIsEllipticMap coe_Δ' map_Δ
coe_Δ' 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Δ' Δ	—	—
c₄_of_char_three 📖	mathematical	—	c₄ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b₂	—	c₄.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
c₄_of_char_two 📖	mathematical	—	c₄ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁	—	c₄.eq_1 b₂_of_char_two Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
c₆_of_char_three 📖	mathematical	—	c₆ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b₂	—	c₆.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
c₆_of_char_two 📖	mathematical	—	c₆ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁	—	c₆.eq_1 b₂_of_char_two Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
ext 📖	—	a₁ a₂ a₃ a₄ a₆	—	—	—
ext_iff 📖	mathematical	—	a₁ a₂ a₃ a₄ a₆	—	ext
instIsEllipticMap 📖	mathematical	—	IsElliptic map	—	map_Δ IsUnit.map isUnit_Δ MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
inv_map_Δ' 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instInv Δ' map instIsEllipticMap DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom RingHom Semiring.toNonAssocSemiring Monoid.toMulOneClass RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass NonAssocSemiring.toMulZeroOneClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	—	instIsEllipticMap MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_Δ' map_inv MonoidHom.instMonoidHomClass
isElliptic_iff 📖	mathematical	—	IsElliptic IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Δ	—	—
isUnit_Δ 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Δ	—	IsElliptic.isUnit
j_eq_zero 📖	mathematical	c₄ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	j	—	j_eq_zero_iff' zero_pow three_ne_zero
j_eq_zero_iff 📖	mathematical	—	j MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing c₄	—	j_eq_zero_iff' pow_eq_zero_iff three_ne_zero
j_eq_zero_iff' 📖	mathematical	—	j MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring c₄	—	j.eq_1 Units.mul_right_eq_zero
j_eq_zero_iff_of_char_three 📖	mathematical	—	j MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing b₂	—	j_eq_zero_iff_of_char_three' pow_eq_zero_iff
j_eq_zero_iff_of_char_three' 📖	mathematical	—	j MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b₂	—	j_of_char_three Units.mul_right_eq_zero
j_eq_zero_iff_of_char_two 📖	mathematical	—	j MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing a₁	—	j_eq_zero_iff_of_char_two' pow_eq_zero_iff
j_eq_zero_iff_of_char_two' 📖	mathematical	—	j MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁	—	j_of_char_two Units.mul_right_eq_zero
j_eq_zero_of_char_three 📖	mathematical	b₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	j	—	j_eq_zero_iff_of_char_three' zero_pow
j_eq_zero_of_char_two 📖	mathematical	a₁ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	j	—	j_eq_zero_iff_of_char_two' zero_pow
j_of_char_three 📖	mathematical	—	j Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv Δ' Monoid.toNatPow b₂	—	j.eq_1 c₄_of_char_three pow_mul
j_of_char_two 📖	mathematical	—	j Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv Δ' Monoid.toNatPow a₁	—	j.eq_1 c₄_of_char_two pow_mul
map_a₁ 📖	mathematical	—	a₁ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—
map_a₂ 📖	mathematical	—	a₂ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—
map_a₃ 📖	mathematical	—	a₃ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—
map_a₄ 📖	mathematical	—	a₄ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—
map_a₆ 📖	mathematical	—	a₆ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—
map_baseChange 📖	mathematical	—	map baseChange RingHomClass.toRingHom AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap_of_tower
map_b₂ 📖	mathematical	—	b₂ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
map_b₄ 📖	mathematical	—	b₄ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
map_b₆ 📖	mathematical	—	b₆ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
map_b₈ 📖	mathematical	—	b₈ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_ofNat
map_c₄ 📖	mathematical	—	c₄ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_b₂ map_b₄ map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
map_c₆ 📖	mathematical	—	c₆ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_b₂ map_b₄ map_b₆ map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_neg map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
map_id 📖	mathematical	—	map RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—
map_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	WeierstrassCurve map	—	ext
map_j 📖	mathematical	—	j map instIsEllipticMap DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	instIsEllipticMap j.eq_1 coe_inv_map_Δ' map_c₄ map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
map_map 📖	mathematical	—	map RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—
map_Δ 📖	mathematical	—	Δ map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_b₂ map_b₈ map_b₄ map_b₆ map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_sub map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_neg map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_ofNat
map_Δ' 📖	mathematical	—	Δ' map instIsEllipticMap DFunLike.coe MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom RingHom Semiring.toNonAssocSemiring Monoid.toMulOneClass RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass NonAssocSemiring.toMulZeroOneClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	—	Units.ext instIsEllipticMap MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coe_map_Δ'
twoTorsionPolynomial_disc 📖	mathematical	—	Cubic.discr CommRing.toRing twoTorsionPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat Δ	—	twoTorsionPolynomial_discr
twoTorsionPolynomial_disc_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	Cubic.discr twoTorsionPolynomial Δ	—	twoTorsionPolynomial_discr_isUnit
twoTorsionPolynomial_disc_ne_zero 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Δ	—	—	twoTorsionPolynomial_discr_ne_zero
twoTorsionPolynomial_disc_ne_zero_of_isElliptic 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	—	twoTorsionPolynomial_discr_ne_zero_of_isElliptic
twoTorsionPolynomial_disc_of_char_three 📖	mathematical	—	Cubic.discr CommRing.toRing twoTorsionPolynomial Δ	—	twoTorsionPolynomial_discr_of_char_three
twoTorsionPolynomial_disc_of_char_two 📖	mathematical	—	Cubic.discr CommRing.toRing twoTorsionPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	twoTorsionPolynomial_discr_of_char_two
twoTorsionPolynomial_discr 📖	mathematical	—	Cubic.discr CommRing.toRing twoTorsionPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat Δ	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.neg_congr
twoTorsionPolynomial_discr_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	Cubic.discr twoTorsionPolynomial Δ	—	Nat.instAtLeastTwoHAddOfNat twoTorsionPolynomial_discr IsUnit.mul_iff instIsDedekindFiniteMonoid Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0 IsUnit.pow
twoTorsionPolynomial_discr_ne_zero 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Δ	—	—	Nat.instAtLeastTwoHAddOfNat IsUnit.ne_zero twoTorsionPolynomial_discr_isUnit
twoTorsionPolynomial_discr_ne_zero_of_isElliptic 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	—	Nat.instAtLeastTwoHAddOfNat twoTorsionPolynomial_discr_ne_zero isUnit_Δ
twoTorsionPolynomial_discr_of_char_three 📖	mathematical	—	Cubic.discr CommRing.toRing twoTorsionPolynomial Δ	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq twoTorsionPolynomial_discr Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
twoTorsionPolynomial_discr_of_char_two 📖	mathematical	—	Cubic.discr CommRing.toRing twoTorsionPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq twoTorsionPolynomial_discr Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
twoTorsionPolynomial_of_char_three 📖	mathematical	—	twoTorsionPolynomial AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing b₂ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup b₄ b₆	—	twoTorsionPolynomial.eq_1 Cubic.ext Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero Nat.cast_one Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_overlap_pf_zero
twoTorsionPolynomial_of_char_two 📖	mathematical	—	twoTorsionPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing b₂ b₆	—	twoTorsionPolynomial.eq_1 Cubic.ext Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero
Δ_of_char_three 📖	mathematical	—	Δ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b₂ b₈ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat b₄	—	Nat.instAtLeastTwoHAddOfNat Δ.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
Δ_of_char_two 📖	mathematical	—	Δ Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring a₁ b₈ a₃	—	Δ.eq_1 b₂_of_char_two b₄_of_char_two b₆_of_char_two Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq CharP.cast_eq_zero Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero

WeierstrassCurve.IsElliptic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.Δ	—	—

(root)

Definitions

Name	Category	Theorems
WeierstrassCurve 📖	CompData	40 math math: WeierstrassCurve.toShortNF_spec, WeierstrassCurve.variableChange_j, WeierstrassCurve.variableChange_a₁, WeierstrassCurve.variableChange_Δ', WeierstrassCurve.toCharNeTwoNF_spec, WeierstrassCurve.toCharThreeNF_spec_of_b₂_ne_zero, WeierstrassCurve.exists_isMinimal, WeierstrassCurve.instIsEllipticHSMulVariableChange, WeierstrassCurve.exists_variableChange_isCharTwoNF, WeierstrassCurve.variableChange_b₈, WeierstrassCurve.IsMinimal.val_Δ_maximal, WeierstrassCurve.variableChange_b₂, WeierstrassCurve.variableChange_b₆, WeierstrassCurve.map_injective, WeierstrassCurve.exists_variableChange_isCharThreeNF, WeierstrassCurve.variableChange_def, WeierstrassCurve.exists_variableChange_isCharNeTwoNF, WeierstrassCurve.toCharTwoJNeZeroNF_spec, WeierstrassCurve.variableChange_a₂, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.exists_variableChange_of_j_eq, WeierstrassCurve.variableChange_c₆, WeierstrassCurve.coe_inv_variableChange_Δ', WeierstrassCurve.inv_variableChange_Δ', WeierstrassCurve.variableChange_Δ, WeierstrassCurve.variableChange_a₄, WeierstrassCurve.isMinimal_iff, WeierstrassCurve.map_variableChange, WeierstrassCurve.exists_isIntegral, WeierstrassCurve.toShortNFOfCharThree_spec, WeierstrassCurve.toCharThreeNF_spec, WeierstrassCurve.toShortNFOfCharThree_a₂, WeierstrassCurve.exists_variableChange_isShortNF, WeierstrassCurve.coe_variableChange_Δ', WeierstrassCurve.toCharTwoNF_spec, WeierstrassCurve.toCharThreeNF_spec_of_b₂_eq_zero, WeierstrassCurve.variableChange_c₄, WeierstrassCurve.variableChange_a₆, WeierstrassCurve.toCharTwoJEqZeroNF_spec, WeierstrassCurve.variableChange_b₄

---

← Back to Index