ModelsWithJ

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

Statistics

Metric	Count
Definitions instInhabitedSubtypeIsElliptic, ofJ, ofJ0, ofJ1728, ofJNe0Or1728	5
Theorems instIsEllipticOfJ, instIsEllipticOfJ0OfFactIsUnitOfNat, instIsEllipticOfJ1728OfFactIsUnitOfNat, instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat, ofJ0_c₄, ofJ0_j, ofJ0_Δ, ofJ1728_c₄, ofJ1728_j, ofJ1728_Δ, ofJNe0Or1728_c₄, ofJNe0Or1728_j, ofJNe0Or1728_Δ, ofJ_0_of_three_eq_zero, ofJ_0_of_three_ne_zero, ofJ_0_of_two_eq_zero, ofJ_1728_of_three_eq_zero, ofJ_1728_of_two_eq_zero, ofJ_1728_of_two_ne_zero, ofJ_j, ofJ_ne_0_ne_1728	21
Total	26

WeierstrassCurve

Definitions

Name	Category	Theorems
instInhabitedSubtypeIsElliptic 📖	CompOp	—
ofJ 📖	CompOp	9 math math: ofJ_j, ofJ_1728_of_two_ne_zero, ofJ_1728_of_two_eq_zero, ofJ_ne_0_ne_1728, ofJ_0_of_three_eq_zero, ofJ_0_of_two_eq_zero, ofJ_0_of_three_ne_zero, instIsEllipticOfJ, ofJ_1728_of_three_eq_zero
ofJ0 📖	CompOp	7 math math: instIsEllipticOfJ0OfFactIsUnitOfNat, ofJ0_Δ, ofJ_1728_of_two_eq_zero, ofJ0_c₄, ofJ0_j, ofJ_0_of_two_eq_zero, ofJ_0_of_three_ne_zero
ofJ1728 📖	CompOp	7 math math: ofJ_1728_of_two_ne_zero, instIsEllipticOfJ1728OfFactIsUnitOfNat, ofJ1728_j, ofJ_0_of_three_eq_zero, ofJ1728_Δ, ofJ_1728_of_three_eq_zero, ofJ1728_c₄
ofJNe0Or1728 📖	CompOp	5 math math: ofJNe0Or1728_Δ, ofJNe0Or1728_c₄, instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat, ofJ_ne_0_ne_1728, ofJNe0Or1728_j

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsEllipticOfJ 📖	mathematical	—	IsElliptic EuclideanDomain.toCommRing Field.toEuclideanDomain ofJ	—	Nat.instAtLeastTwoHAddOfNat IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd 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.add_mul 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.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isNat_add 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 ofJ_0_of_three_eq_zero instIsEllipticOfJ1728OfFactIsUnitOfNat Ne.isUnit ofJ_0_of_three_ne_zero instIsEllipticOfJ0OfFactIsUnitOfNat Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero ofJ_1728_of_two_ne_zero sub_ne_zero ofJ_ne_0_ne_1728 instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat
instIsEllipticOfJ0OfFactIsUnitOfNat 📖	mathematical	—	IsElliptic ofJ0	—	Nat.instAtLeastTwoHAddOfNat isElliptic_iff ofJ0_Δ 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.bit1 IsUnit.neg IsUnit.pow Fact.out
instIsEllipticOfJ1728OfFactIsUnitOfNat 📖	mathematical	—	IsElliptic ofJ1728	—	Nat.instAtLeastTwoHAddOfNat isElliptic_iff ofJ1728_Δ 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.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit0 IsUnit.neg IsUnit.pow Fact.out
instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat 📖	mathematical	—	IsElliptic ofJNe0Or1728	—	Nat.instAtLeastTwoHAddOfNat isElliptic_iff ofJNe0Or1728_Δ IsUnit.mul IsUnit.pow Fact.out
ofJ0_c₄ 📖	mathematical	—	c₄ ofJ0 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	ofJ0.eq_1 c₄.eq_1 b₂.eq_1 b₄.eq_1 Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.zero_natPow Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one
ofJ0_j 📖	mathematical	—	j ofJ0 instIsEllipticOfJ0OfFactIsUnitOfNat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Nat.instAtLeastTwoHAddOfNat instIsEllipticOfJ0OfFactIsUnitOfNat j.eq_1 ofJ0_c₄ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_zero_add
ofJ0_Δ 📖	mathematical	—	Δ ofJ0 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat ofJ0.eq_1 Δ.eq_1 b₂.eq_1 b₄.eq_1 b₆.eq_1 b₈.eq_1 Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.zero_natPow Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Mathlib.Meta.NormNum.one_natPow
ofJ1728_c₄ 📖	mathematical	—	c₄ ofJ1728 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat ofJ1728.eq_1 c₄.eq_1 b₂.eq_1 b₄.eq_1 Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.zero_natPow Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Mathlib.Meta.NormNum.isInt_neg
ofJ1728_j 📖	mathematical	—	j ofJ1728 instIsEllipticOfJ1728OfFactIsUnitOfNat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat instIsEllipticOfJ1728OfFactIsUnitOfNat j.eq_1 Units.inv_mul_eq_iff_eq_mul ofJ1728_c₄ coe_Δ' ofJ1728_Δ Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.intPow_negOfNat_bit1 Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.isInt_mul
ofJ1728_Δ 📖	mathematical	—	Δ ofJ1728 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat ofJ1728.eq_1 Δ.eq_1 b₂.eq_1 b₄.eq_1 b₆.eq_1 b₈.eq_1 Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.zero_natPow Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1
ofJNe0Or1728_c₄ 📖	mathematical	—	c₄ ofJNe0Or1728 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero
ofJNe0Or1728_j 📖	mathematical	—	j ofJNe0Or1728 instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat	—	Nat.instAtLeastTwoHAddOfNat instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat j.eq_1 Units.inv_mul_eq_iff_eq_mul ofJNe0Or1728_c₄ coe_Δ' ofJNe0Or1728_Δ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_bit0
ofJNe0Or1728_Δ 📖	mathematical	—	Δ ofJNe0Or1728 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne 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.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow
ofJ_0_of_three_eq_zero 📖	mathematical	instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	ofJ ofJ1728	—	Nat.instAtLeastTwoHAddOfNat ofJ.eq_1
ofJ_0_of_three_ne_zero 📖	mathematical	—	ofJ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain ofJ0	—	Nat.instAtLeastTwoHAddOfNat ofJ.eq_1
ofJ_0_of_two_eq_zero 📖	mathematical	instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	ofJ ofJ0	—	Nat.instAtLeastTwoHAddOfNat ofJ.eq_1 one_ne_zero NeZero.one EuclideanDomain.toNontrivial Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd 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.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
ofJ_1728_of_three_eq_zero 📖	mathematical	instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	ofJ ofJ1728	—	Nat.instAtLeastTwoHAddOfNat ofJ.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq 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.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
ofJ_1728_of_two_eq_zero 📖	mathematical	instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	ofJ ofJ0	—	Nat.instAtLeastTwoHAddOfNat ofJ.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq 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.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 one_ne_zero NeZero.one EuclideanDomain.toNontrivial Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isNat_add
ofJ_1728_of_two_ne_zero 📖	mathematical	—	ofJ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat ofJ1728 EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Nat.instAtLeastTwoHAddOfNat ofJ_1728_of_three_eq_zero ofJ.eq_1 Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit0 mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain pow_ne_zero isReduced_of_noZeroDivisors
ofJ_j 📖	mathematical	—	j EuclideanDomain.toCommRing Field.toEuclideanDomain ofJ instIsEllipticOfJ	—	instIsEllipticOfJ Nat.instAtLeastTwoHAddOfNat IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd 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.add_mul 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.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isNat_add 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 j.congr_simp ofJ_0_of_three_eq_zero ofJ1728_j Mathlib.Tactic.LinearCombination.mul_const_eq Ne.isUnit ofJ_0_of_three_ne_zero ofJ0_j Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero ofJ_1728_of_two_ne_zero sub_ne_zero ofJ_ne_0_ne_1728 ofJNe0Or1728_j
ofJ_ne_0_ne_1728 📖	mathematical	—	ofJ ofJNe0Or1728 EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Nat.instAtLeastTwoHAddOfNat ofJ.eq_1

---

← Back to Index