QHat

Statistics

Metric	Count
Definitions `QHat`, `IsCoprime`, `i₁`, `i₂`, `ratsub`, `unitsratsub`, `unitszHatsub`, `unitszsub`, `zHatsub`, `zsub`, `ZHat`, `commRing`, `e`, `instDFunLikePNatZModVal`, `instCommRingZHat`	15
Theorems `intCast_tmul_one`, `one_tmul_intCast`, `one_tmul_natCast`, `sum_factorial_lt_factorial_succ`, `sum_factorial_lt_two_mul_factorial`, `lcm_comm`, `isUnit_natAbs`, `canonicalForm`, `injective_rat`, `injective_zHat`, `isCoprime_iff_coprime`, `isUnit_iff_coprime`, `lowestTerms`, `nontrivial_QHat`, `rat_join_zHat`, `rat_meet_zHat`, `unitsrat_join_unitszHat`, `unitsrat_meet_unitszHat`, `ZHat_flat`, `charZero`, `e_def`, `e_factorial_succ`, `e_not_in_Int`, `eq_zero_of_mul_eq_zero`, `ext`, `ext_iff`, `intCast_val`, `multiples`, `natCast_val`, `nat_dense`, `nat_mul_apply`, `nontrivial`, `ofNat_val`, `one_val`, `pnat_mul_apply`, `prop`, `torsionfree`, `torsionfree_aux`, `y_mul_N_eq_z`, `zeroNeOne`, `zero_val`	41
Total	56

Algebra.TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast_tmul_one` 📖	—	—	—	—	—
`one_tmul_intCast` 📖	—	—	—	—	—
`one_tmul_natCast` 📖	—	—	—	—	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_factorial_lt_factorial_succ` 📖	—	—	—	—	—
`sum_factorial_lt_two_mul_factorial` 📖	—	—	—	—	`sum_factorial_lt_factorial_succ`

QHat

Definitions

Name	Category	Theorems
`IsCoprime` 📖	MathDef	2 math math: `isCoprime_iff_coprime`, `lowestTerms`
`i₁` 📖	CompOp	1 math math: `injective_rat`
`i₂` 📖	CompOp	1 math math: `injective_zHat`
`ratsub` 📖	CompOp	2 math math: `rat_join_zHat`, `rat_meet_zHat`
`unitsratsub` 📖	CompOp	2 math math: `unitsrat_meet_unitszHat`, `unitsrat_join_unitszHat`
`unitszHatsub` 📖	CompOp	2 math math: `unitsrat_meet_unitszHat`, `unitsrat_join_unitszHat`
`unitszsub` 📖	CompOp	1 math math: `unitsrat_meet_unitszHat`
`zHatsub` 📖	CompOp	2 math math: `rat_join_zHat`, `rat_meet_zHat`
`zsub` 📖	CompOp	1 math math: `rat_meet_zHat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canonicalForm` 📖	mathematical	—	`ZHat` `ZHat.commRing`	—	—
`injective_rat` 📖	mathematical	—	`QHat` `ZHat` `ZHat.commRing` `i₁`	—	`nontrivial_QHat`
`injective_zHat` 📖	mathematical	—	`ZHat` `QHat` `ZHat.commRing` `i₂`	—	`ZHat.ZHat_flat`
`isCoprime_iff_coprime` 📖	mathematical	—	`IsCoprime` `ZHat` `ZHat.instDFunLikePNatZModVal`	—	`isUnit_iff_coprime`
`isUnit_iff_coprime` 📖	—	—	—	—	—
`lowestTerms` 📖	mathematical	—	`IsCoprime` `ZHat` `ZHat.commRing`	—	`canonicalForm` `isCoprime_iff_coprime` `ZHat.prop` `ZHat.multiples` `injective_zHat` `ZHat.torsionfree` `PNat.lcm_comm`
`nontrivial_QHat` 📖	mathematical	—	`QHat`	—	`injective_zHat` `ZHat.zeroNeOne`
`rat_join_zHat` 📖	mathematical	—	`QHat` `ZHat` `ZHat.commRing` `ratsub` `zHatsub`	—	`canonicalForm` `ZHat.nat_dense`
`rat_meet_zHat` 📖	mathematical	—	`QHat` `ZHat` `ZHat.commRing` `ratsub` `zHatsub` `zsub`	—	`lowestTerms` `Algebra.TensorProduct.one_tmul_intCast`
`unitsrat_join_unitszHat` 📖	mathematical	—	`QHat` `ZHat` `ZHat.commRing` `unitsratsub` `unitszHatsub`	—	`canonicalForm` `injective_zHat` `Algebra.TensorProduct.one_tmul_natCast` `ZHat.multiples` `ZHat.eq_zero_of_mul_eq_zero` `Algebra.TensorProduct.one_tmul_intCast`
`unitsrat_meet_unitszHat` 📖	mathematical	—	`QHat` `ZHat` `ZHat.commRing` `unitsratsub` `unitszHatsub` `unitszsub`	—	`rat_meet_zHat` `nontrivial_QHat` `IsCoprime.eq_1` `ZHat.intCast_val` `ZMod.isUnit_natAbs` `lowestTerms` `Algebra.TensorProduct.one_tmul_intCast`

QHat.PNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lcm_comm` 📖	—	—	—	—	—

QHat.ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_natAbs` 📖	—	—	—	—	—

ZHat

Definitions

Name	Category	Theorems
`commRing` 📖	CompOp	15 math math: `QHat.unitsrat_meet_unitszHat`, `nat_dense`, `QHat.unitsrat_join_unitszHat`, `multiples`, `ZHat_flat`, `pnat_mul_apply`, `nat_mul_apply`, `QHat.injective_rat`, `QHat.canonicalForm`, `charZero`, `QHat.injective_zHat`, `QHat.lowestTerms`, `QHat.rat_join_zHat`, `torsionfree`, `QHat.rat_meet_zHat`
`e` 📖	CompOp	2 math math: `e_factorial_succ`, `e_def`
`instDFunLikePNatZModVal` 📖	CompOp	13 math math: `e_factorial_succ`, `multiples`, `ext_iff`, `prop`, `QHat.isCoprime_iff_coprime`, `pnat_mul_apply`, `nat_mul_apply`, `ofNat_val`, `e_def`, `natCast_val`, `one_val`, `zero_val`, `intCast_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ZHat_flat` 📖	mathematical	—	`ZHat` `commRing`	—	`eq_zero_of_mul_eq_zero`
`charZero` 📖	mathematical	—	`ZHat` `commRing`	—	`natCast_val` `ext_iff`
`e_def` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `e`	—	—
`e_factorial_succ` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `e`	—	—
`e_not_in_Int` 📖	—	—	—	—	`Nat.sum_factorial_lt_factorial_succ` `e_factorial_succ` `Nat.sum_factorial_lt_two_mul_factorial` `intCast_val`
`eq_zero_of_mul_eq_zero` 📖	—	`ZHat` `commRing`	—	—	`ext` `zero_val` `prop` `torsionfree_aux` `pnat_mul_apply`
`ext` 📖	—	`ZHat` `instDFunLikePNatZModVal`	—	—	—
`ext_iff` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal`	—	`ext`
`intCast_val` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `instCommRingZHat`	—	—
`multiples` 📖	mathematical	—	`ZHat` `commRing` `instDFunLikePNatZModVal`	—	`prop` `ext` `y_mul_N_eq_z`
`natCast_val` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `instCommRingZHat`	—	—
`nat_dense` 📖	mathematical	—	`ZHat` `commRing`	—	`multiples`
`nat_mul_apply` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `commRing`	—	—
`nontrivial` 📖	mathematical	—	`ZHat`	—	`zeroNeOne`
`ofNat_val` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `instCommRingZHat`	—	—
`one_val` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `instCommRingZHat`	—	—
`pnat_mul_apply` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `commRing`	—	—
`prop` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal`	—	—
`torsionfree` 📖	mathematical	—	`ZHat` `commRing`	—	`eq_zero_of_mul_eq_zero`
`torsionfree_aux` 📖	—	—	—	—	—
`y_mul_N_eq_z` 📖	—	`ZHat` `instDFunLikePNatZModVal`	—	—	`prop`
`zeroNeOne` 📖	—	—	—	—	`one_val` `zero_val`
`zero_val` 📖	mathematical	—	`ZHat` `instDFunLikePNatZModVal` `instCommRingZHat`	—	—

(root)

Definitions

Name	Category	Theorems
`QHat` 📖	CompOp	7 math math: `QHat.unitsrat_meet_unitszHat`, `QHat.unitsrat_join_unitszHat`, `QHat.injective_rat`, `QHat.injective_zHat`, `QHat.rat_join_zHat`, `QHat.nontrivial_QHat`, `QHat.rat_meet_zHat`
`ZHat` 📖	CompOp	26 math math: `QHat.unitsrat_meet_unitszHat`, `ZHat.nat_dense`, `QHat.unitsrat_join_unitszHat`, `ZHat.e_factorial_succ`, `ZHat.multiples`, `ZHat.ext_iff`, `ZHat.prop`, `ZHat.ZHat_flat`, `QHat.isCoprime_iff_coprime`, `ZHat.pnat_mul_apply`, `ZHat.nat_mul_apply`, `QHat.injective_rat`, `QHat.canonicalForm`, `ZHat.ofNat_val`, `ZHat.charZero`, `ZHat.e_def`, `QHat.injective_zHat`, `ZHat.natCast_val`, `QHat.lowestTerms`, `ZHat.one_val`, `ZHat.nontrivial`, `ZHat.zero_val`, `QHat.rat_join_zHat`, `ZHat.torsionfree`, `ZHat.intCast_val`, `QHat.rat_meet_zHat`
`instCommRingZHat` 📖	CompOp	5 math math: `ZHat.ofNat_val`, `ZHat.natCast_val`, `ZHat.one_val`, `ZHat.zero_val`, `ZHat.intCast_val`

---

← Back to Index