Root

📁 Source: Mathlib/Data/Nat/Factorization/Root.lean

Statistics

Metric	Count
Definitions `ceilRoot`, `floorRoot`	2
Theorems `ceilRoot_def`, `ceilRoot_eq_zero`, `ceilRoot_ne_zero`, `ceilRoot_one_left`, `ceilRoot_one_right`, `ceilRoot_pow_self`, `ceilRoot_zero_left`, `ceilRoot_zero_right`, `dvd_ceilRoot_pow`, `dvd_pow_iff_ceilRoot_dvd`, `factorization_ceilRoot`, `factorization_floorRoot`, `floorRoot_def`, `floorRoot_eq_zero`, `floorRoot_ne_zero`, `floorRoot_one_left`, `floorRoot_one_right`, `floorRoot_pow_dvd`, `floorRoot_pow_self`, `floorRoot_zero_left`, `floorRoot_zero_right`, `pow_dvd_iff_dvd_floorRoot`	22
Total	24

Nat

Definitions

Name	Category	Theorems
`ceilRoot` 📖	CompOp	10 math math: `ceilRoot_def`, `ceilRoot_one_left`, `factorization_ceilRoot`, `ceilRoot_eq_zero`, `dvd_pow_iff_ceilRoot_dvd`, `ceilRoot_zero_left`, `ceilRoot_zero_right`, `ceilRoot_one_right`, `ceilRoot_pow_self`, `dvd_ceilRoot_pow`
`floorRoot` 📖	CompOp	10 math math: `floorRoot_eq_zero`, `floorRoot_zero_left`, `floorRoot_zero_right`, `pow_dvd_iff_dvd_floorRoot`, `floorRoot_one_right`, `floorRoot_one_left`, `factorization_floorRoot`, `floorRoot_def`, `floorRoot_pow_self`, `floorRoot_pow_dvd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ceilRoot_def` 📖	mathematical	—	`ceilRoot` `Finsupp.prod` `MulZeroClass.toZero` `instMulZeroClass` `instCommMonoid` `CeilDiv.ceilDiv` `Finsupp` `instAddCommMonoid` `instPartialOrder` `Finsupp.instAddCommMonoid` `Finsupp.partialorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.smulZeroClass` `DistribSMul.toSMulZeroClass` `instAddMonoid` `instDistribSMul` `instNonUnitalNonAssocSemiring` `Finsupp.instCeilDiv` `instCeilDiv` `factorization` `Monoid.toNatPow` `instMonoid`	—	`Finsupp.prod_mapRange_index` `pow_zero` `zero_ceilDiv`
`ceilRoot_eq_zero` 📖	mathematical	—	`ceilRoot`	—	`Iff.not_right` `ceilRoot_ne_zero`
`ceilRoot_ne_zero` 📖	—	—	—	—	`ceilRoot_def` `instNontrivial` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `factorization_zero_right` `zero_ceilDiv`
`ceilRoot_one_left` 📖	mathematical	—	`ceilRoot`	—	`add_tsub_cancel_right` `instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `factorization_prod_pow_eq_self`
`ceilRoot_one_right` 📖	mathematical	—	`ceilRoot`	—	`factorization_one`
`ceilRoot_pow_self` 📖	mathematical	—	`ceilRoot` `Monoid.toNatPow` `instMonoid`	—	`ceilRoot_def` `factorization_pow` `smul_ceilDiv` `instPosSMulMonoNatOfIsOrderedAddMonoid` `Finsupp.isOrderedAddMonoid` `instIsOrderedAddMonoid` `Finsupp.instPosSMulReflectLE` `PosSMulStrictMono.toPosSMulReflectLE` `StrictOrderedSemiring.toPosSMulStrictMonoNat` `instIsStrictOrderedRing` `pos_iff_ne_zero` `instCanonicallyOrderedAdd` `factorization_prod_pow_eq_self`
`ceilRoot_zero_left` 📖	mathematical	—	`ceilRoot`	—	—
`ceilRoot_zero_right` 📖	mathematical	—	`ceilRoot`	—	—
`dvd_ceilRoot_pow` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `ceilRoot`	—	`dvd_pow_iff_ceilRoot_dvd` `dvd_rfl`
`dvd_pow_iff_ceilRoot_dvd` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `ceilRoot`	—	`eq_or_ne` `ceilRoot_zero_right` `zero_pow` `factorization_le_iff_dvd` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `ceilRoot_ne_zero` `factorization_pow` `factorization_ceilRoot` `ceilDiv_le_iff_le_smul` `pos_iff_ne_zero`
`factorization_ceilRoot` 📖	mathematical	—	`factorization` `ceilRoot` `CeilDiv.ceilDiv` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `instAddCommMonoid` `instPartialOrder` `Finsupp.instAddCommMonoid` `Finsupp.partialorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.smulZeroClass` `DistribSMul.toSMulZeroClass` `instAddMonoid` `instDistribSMul` `instNonUnitalNonAssocSemiring` `Finsupp.instCeilDiv` `instCeilDiv`	—	`ceilRoot_def` `factorization_zero` `ceilDiv_of_nonpos` `zero_ceilDiv` `prod_pow_factorization_eq_self` `Finsupp.support_ceilDiv_subset`
`factorization_floorRoot` 📖	mathematical	—	`factorization` `floorRoot` `FloorDiv.floorDiv` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `instAddCommMonoid` `instPartialOrder` `Finsupp.instAddCommMonoid` `Finsupp.partialorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.smulZeroClass` `DistribSMul.toSMulZeroClass` `instAddMonoid` `instDistribSMul` `instNonUnitalNonAssocSemiring` `Finsupp.instFloorDiv` `instFloorDiv`	—	`floorRoot_def` `factorization_zero` `floorDiv_of_nonpos` `zero_floorDiv` `prod_pow_factorization_eq_self` `Finsupp.support_floorDiv_subset`
`floorRoot_def` 📖	mathematical	—	`floorRoot` `Finsupp.prod` `MulZeroClass.toZero` `instMulZeroClass` `instCommMonoid` `FloorDiv.floorDiv` `Finsupp` `instAddCommMonoid` `instPartialOrder` `Finsupp.instAddCommMonoid` `Finsupp.partialorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.smulZeroClass` `DistribSMul.toSMulZeroClass` `instAddMonoid` `instDistribSMul` `instNonUnitalNonAssocSemiring` `Finsupp.instFloorDiv` `instFloorDiv` `factorization` `Monoid.toNatPow` `instMonoid`	—	`Finsupp.prod_mapRange_index` `pow_zero` `zero_floorDiv`
`floorRoot_eq_zero` 📖	mathematical	—	`floorRoot`	—	`Iff.not_right` `floorRoot_ne_zero`
`floorRoot_ne_zero` 📖	—	—	—	—	`instNontrivial` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `factorization_zero_right`
`floorRoot_one_left` 📖	mathematical	—	`floorRoot`	—	`factorization_prod_pow_eq_self`
`floorRoot_one_right` 📖	mathematical	—	`floorRoot`	—	`factorization_one`
`floorRoot_pow_dvd` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `floorRoot`	—	`pow_dvd_iff_dvd_floorRoot` `dvd_rfl`
`floorRoot_pow_self` 📖	mathematical	—	`floorRoot` `Monoid.toNatPow` `instMonoid`	—	`floorRoot_def` `factorization_pow` `smul_floorDiv` `instPosSMulMonoNatOfIsOrderedAddMonoid` `Finsupp.isOrderedAddMonoid` `instIsOrderedAddMonoid` `Finsupp.instPosSMulReflectLE` `PosSMulStrictMono.toPosSMulReflectLE` `StrictOrderedSemiring.toPosSMulStrictMonoNat` `instIsStrictOrderedRing` `pos_iff_ne_zero` `instCanonicallyOrderedAdd` `factorization_prod_pow_eq_self`
`floorRoot_zero_left` 📖	mathematical	—	`floorRoot`	—	—
`floorRoot_zero_right` 📖	mathematical	—	`floorRoot`	—	—
`pow_dvd_iff_dvd_floorRoot` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `floorRoot`	—	`eq_or_ne` `pow_zero` `Unique.instSubsingleton` `floorRoot_zero_left` `floorRoot_zero_right` `zero_pow` `factorization_le_iff_dvd` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `floorRoot_ne_zero` `factorization_pow` `factorization_floorRoot` `le_floorDiv_iff_smul_le` `pos_iff_ne_zero`

---

← Back to Index