PythagoreanTriples

📁 Source: Mathlib/NumberTheory/PythagoreanTriples.lean

Statistics

Metric	Count
Definitions PythagoreanTriple, IsClassified, IsPrimitiveClassified, circleEquivGen	4
Theorems sq_ne_two_mod_four, classification, classified, coprime_classification, coprime_classification', coprime_of_coprime, eq, even_odd_of_coprime, gcd_dvd, isClassified_of_isPrimitiveClassified, isClassified_of_normalize_isPrimitiveClassified, isPrimitiveClassified_aux, isPrimitiveClassified_of_coprime, isPrimitiveClassified_of_coprime_of_odd_of_pos, isPrimitiveClassified_of_coprime_of_pos, isPrimitiveClassified_of_coprime_of_zero_left, mul, mul_iff, mul_isClassified, ne_zero_of_coprime, normalize, zero, circleEquivGen_apply, circleEquivGen_symm_apply, pythagoreanTriple_comm, sq_ne_two_fin_zmod_four	26
Total	30

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sq_ne_two_mod_four 📖	—	—	—	—	ZMod.intCast_eq_intCast_iff' Nat.instAtLeastTwoHAddOfNat cast_mul cast_ofNat sq_ne_two_fin_zmod_four

PythagoreanTriple

Definitions

Name	Category	Theorems
IsClassified 📖	MathDef	3 math math: isClassified_of_normalize_isPrimitiveClassified, classified, isClassified_of_isPrimitiveClassified
IsPrimitiveClassified 📖	MathDef	5 math math: isPrimitiveClassified_of_coprime, isPrimitiveClassified_of_coprime_of_pos, isPrimitiveClassified_of_coprime_of_odd_of_pos, isPrimitiveClassified_of_coprime_of_zero_left, isPrimitiveClassified_aux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
classification 📖	mathematical	—	PythagoreanTriple Monoid.toNatPow Int.instMonoid	—	classified sq eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr 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_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.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.mul_pf_right Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add 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 neg_mul eq_or_eq_neg_of_sq_eq_sq IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Mathlib.Tactic.Ring.neg_congr
classified 📖	mathematical	PythagoreanTriple	IsClassified	—	one_pow zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat sub_zero mul_one MulZeroClass.mul_zero Int.natAbs_of_isUnit isClassified_of_normalize_isPrimitiveClassified isPrimitiveClassified_of_coprime normalize Int.gcd_div_gcd_div_gcd
coprime_classification 📖	mathematical	—	PythagoreanTriple Monoid.toNatPow Int.instMonoid	—	isPrimitiveClassified_of_coprime sq eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_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.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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add 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 neg_add_rev eq_or_eq_neg_of_sq_eq_sq IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Mathlib.Tactic.Ring.neg_congr
coprime_classification' 📖	mathematical	PythagoreanTriple	Monoid.toNatPow Int.instMonoid	—	coprime_classification le_or_gt not_lt neg_nonpos Int.instAddLeftMono add_nonneg Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul zero_ne_one mul_assoc neg_sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.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.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat
coprime_of_coprime 📖	—	PythagoreanTriple	—	—	Nat.Prime.not_coprime_iff_dvd Nat.Prime.not_dvd_one Int.Prime.dvd_natAbs_of_coe_dvd_sq sq eq_sub_of_add_eq dvd_sub Dvd.dvd.mul_right Int.natCast_dvd
eq 📖	—	PythagoreanTriple	—	—	—
even_odd_of_coprime 📖	—	PythagoreanTriple	—	—	Int.emod_two_eq_zero_or_one Int.natCast_dvd exists_eq_mul_left_of_dvd sub_eq_iff_eq_add Int.sq_ne_two_mod_four eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_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.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf zero_add
gcd_dvd 📖	—	PythagoreanTriple	—	—	MulZeroClass.mul_zero add_zero IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Int.exists_gcd_one' one_mul two_ne_zero sq eq Mathlib.Tactic.Ring.of_eq 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.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_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 dvd_mul_right
isClassified_of_isPrimitiveClassified 📖	mathematical	PythagoreanTriple IsPrimitiveClassified	IsClassified	—	—
isClassified_of_normalize_isPrimitiveClassified 📖	mathematical	PythagoreanTriple IsPrimitiveClassified normalize	IsClassified	—	normalize mul gcd_dvd mul_isClassified isClassified_of_isPrimitiveClassified
isPrimitiveClassified_aux 📖	mathematical	PythagoreanTriple Monoid.toNatPow Int.instMonoid Rat.monoid	IsPrimitiveClassified	—	ne_of_gt coprime_of_coprime Rat.instCharZero div_left_inj' Nat.instAtLeastTwoHAddOfNat Int.cast_ofNat
isPrimitiveClassified_of_coprime 📖	mathematical	PythagoreanTriple	IsPrimitiveClassified	—	isPrimitiveClassified_of_coprime_of_pos mul_neg neg_mul neg_neg eq lt_of_le_of_ne le_neg Int.instAddLeftMono covariant_swap_add_of_covariant_add ne_zero_of_coprime
isPrimitiveClassified_of_coprime_of_odd_of_pos 📖	mathematical	PythagoreanTriple	IsPrimitiveClassified	—	isPrimitiveClassified_of_coprime_of_zero_left Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Int.cast_pos IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing IsOrderedRing.toZeroLEOneClass NeZero.one Rat.nontrivial Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero GroupWithZero.toNontrivial sq Rat.instCharZero MulZeroClass.mul_zero Mathlib.Tactic.Contrapose.contrapose₄ eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors AddGroup.existsAddOfLE add_eq_right AddRightCancelSemigroup.toIsRightCancelAdd one_pow neg_sq lt_add_of_pos_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono covariant_swap_add_of_covariant_add Rat.instAddLeftMono zero_lt_one Rat.instZeroLEOneClass NeZero.charZero_one sq_nonneg Rat.instPosMulMono Equiv.apply_symm_apply Nat.cast_zero Int.instCharZero Rat.num_div_den add_pos_of_pos_of_nonneg Int.instAddLeftMono pow_pos IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' Int.instZeroLEOneClass Even.pow_nonneg Nat.instAtLeastTwoHAddOfNat even_two_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_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.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.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Meta.NormNum.isNat_eq_false Int.emod_two_eq_zero_or_one isPrimitiveClassified_aux coprime_of_coprime
isPrimitiveClassified_of_coprime_of_pos 📖	mathematical	PythagoreanTriple	IsPrimitiveClassified	—	even_odd_of_coprime isPrimitiveClassified_of_coprime_of_odd_of_pos symm
isPrimitiveClassified_of_coprime_of_zero_left 📖	mathematical	PythagoreanTriple	IsPrimitiveClassified	—	—
mul 📖	—	PythagoreanTriple	—	—	Mathlib.Tactic.Ring.of_eq 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.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_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 eq
mul_iff 📖	mathematical	—	PythagoreanTriple	—	mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero Int.instIsCancelMulZero mul_ne_zero IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right mul
mul_isClassified 📖	mathematical	PythagoreanTriple IsClassified	mul	—	mul
ne_zero_of_coprime 📖	—	PythagoreanTriple	—	—	eq sq one_ne_zero Int.ne_zero_of_gcd lt_add_of_pos_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono sq_pos_of_ne_zero Int.instIsStrictOrderedRing AddGroup.existsAddOfLE sq_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing lt_add_of_le_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Mathlib.Meta.NormNum.isNat_lt_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_mul
normalize 📖	—	PythagoreanTriple	—	—	MulZeroClass.mul_zero add_zero IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE zero gcd_dvd Int.exists_gcd_one' Nat.cast_zero Int.instCharZero pos_iff_ne_zero Nat.instCanonicallyOrderedAdd one_mul mul_iff mul_comm
zero 📖	mathematical	—	PythagoreanTriple	—	MulZeroClass.zero_mul zero_add

(root)

Definitions

Name	Category	Theorems
PythagoreanTriple 📖	MathDef	5 math math: PythagoreanTriple.mul_iff, PythagoreanTriple.classification, PythagoreanTriple.coprime_classification, PythagoreanTriple.zero, pythagoreanTriple_comm
circleEquivGen 📖	CompOp	2 math math: circleEquivGen_symm_apply, circleEquivGen_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleEquivGen_apply 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike circleEquivGen DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	—
circleEquivGen_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup EquivLike.toFunLike Equiv.instEquivLike Equiv.symm circleEquivGen DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	—
pythagoreanTriple_comm 📖	mathematical	—	PythagoreanTriple	—	add_comm
sq_ne_two_fin_zmod_four 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat Fintype.complete

---

← Back to Index