Abs

📁 Source: Mathlib/Algebra/Order/Ring/Abs.lean

Statistics

Metric	Count
Definitions `absHom`	1
Theorems `mod_even`, `mod_even_iff`, `pow_abs`, `le_abs_of_dvd`, `mod_even`, `mod_even_iff`, `ne_two_of_dvd_nat`, `of_dvd_nat`, `abs_dvd`, `abs_dvd_abs`, `abs_dvd_self`, `abs_eq_iff_mul_self_eq`, `abs_le_iff_mul_self_le`, `abs_le_of_sq_le_sq`, `abs_le_of_sq_le_sq'`, `abs_le_one_iff_mul_self_le_one`, `abs_lt_iff_mul_self_lt`, `abs_lt_of_sq_lt_sq`, `abs_lt_of_sq_lt_sq'`, `abs_mul`, `abs_mul_abs_self`, `abs_mul_self`, `abs_neg_one_pow`, `abs_one`, `abs_pow`, `abs_pow_eq_one`, `abs_pow_sub_pow_le`, `abs_sq`, `abs_sub_sq`, `abs_two`, `abs_unit_intCast`, `abs_zsmul`, `dvd_abs`, `exists_abs_lt`, `le_of_sq_le_sq`, `mabs_zpow`, `odd_abs`, `one_le_sq_iff_one_le_abs`, `one_lt_sq_iff_one_lt_abs`, `pow_abs`, `pow_eq_neg_one_iff`, `pow_eq_neg_pow_iff`, `pow_eq_one_iff_cases`, `pow_eq_one_iff_of_ne_zero`, `pow_eq_pow_iff_cases`, `pow_eq_pow_iff_of_ne_zero`, `self_dvd_abs`, `sq_abs`, `sq_eq_sq_iff_abs_eq_abs`, `sq_le_one_iff_abs_le_one`, `sq_le_sq`, `sq_le_sq'`, `sq_lt_one_iff_abs_lt_one`, `sq_lt_sq`, `sq_lt_sq'`	55
Total	56

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mod_even` 📖	—	`Even`	—	—	`mod_even_iff`
`mod_even_iff` 📖	—	`Even`	—	—	`Nat.even_sub` `Nat.instAtLeastTwoHAddOfNat` `even_iff_two_dvd` `Dvd.dvd.trans`
`pow_abs` 📖	mathematical	`Even`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_pow` `abs_eq_self` `IsOrderedRing.toIsOrderedAddMonoid` `pow_nonneg` `AddGroup.existsAddOfLE`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_abs_of_dvd` 📖	mathematical	—	`abs` `instLatticeInt` `instAddGroup`	—	`instAddLeftMono`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mod_even` 📖	—	`Odd` `Nat.instSemiring` `Even`	—	—	`mod_even_iff`
`mod_even_iff` 📖	mathematical	`Even`	`Odd` `Nat.instSemiring`	—	`Nat.even_sub'` `Nat.instAtLeastTwoHAddOfNat` `even_iff_two_dvd` `Dvd.dvd.trans`
`ne_two_of_dvd_nat` 📖	—	`Odd` `Nat.instSemiring`	—	—	`of_dvd_nat`
`of_dvd_nat` 📖	—	`Odd` `Nat.instSemiring`	—	—	`Nat.not_even_iff_odd` `Dvd.dvd.even`

(root)

Definitions

Name	Category	Theorems
`absHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_dvd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_choice`
`abs_dvd_abs` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_dvd` `dvd_abs`
`abs_dvd_self` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_dvd` `dvd_refl`
`abs_eq_iff_mul_self_eq` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`abs_mul_abs_self` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`abs_le_iff_mul_self_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`abs_mul_abs_self` `mul_self_le_mul_self_iff` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`abs_le_of_sq_le_sq` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sq_le_sq`
`abs_le_of_sq_le_sq'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`abs_le` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `abs_le_of_sq_le_sq`
`abs_le_one_iff_mul_self_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`abs_one` `IsStrictOrderedRing.toIsOrderedRing` `one_mul` `abs_le_iff_mul_self_le`
`abs_lt_iff_mul_self_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`abs_mul_abs_self` `mul_self_lt_mul_self_iff` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`abs_lt_of_sq_lt_sq` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sq_lt_sq`
`abs_lt_of_sq_lt_sq'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`abs_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `abs_lt_of_sq_lt_sq`
`abs_mul` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`abs_eq` `IsOrderedRing.toIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `le_total` `abs_of_nonpos` `mul_neg` `neg_mul` `neg_neg` `abs_of_nonneg`
`abs_mul_abs_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_by_cases` `neg_mul_neg`
`abs_mul_self` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`abs_mul` `abs_mul_abs_self`
`abs_neg_one_pow` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`pow_abs` `abs_neg` `abs_one` `one_pow`
`abs_one` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `zero_le_one` `IsOrderedRing.toZeroLEOneClass`
`abs_pow` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`MonoidHom.map_pow`
`abs_pow_eq_one` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`pow_abs` `IsStrictOrderedRing.toIsOrderedRing` `one_pow` `pow_left_inj₀` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `zero_le_one` `IsStrictOrderedRing.toZeroLEOneClass`
`abs_pow_sub_pow_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`pow_zero` `sub_self` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `Nat.cast_zero` `MulZeroClass.mul_zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `mul_one` `abs_mul` `mul_assoc` `Nat.cast_succ` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `abs_nonneg` `covariant_swap_add_of_covariant_add`
`abs_sq` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`sq` `abs_mul_self`
`abs_sub_sq` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`abs_mul_abs_self` `sub_eq_add_neg` `mul_add` `Distrib.leftDistribClass` `mul_comm` `mul_neg` `neg_neg` `add_comm` `add_left_comm` `mul_one` `neg_add_rev` `add_assoc`
`abs_two` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`abs_of_nonneg` `Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `zero_le_two` `IsOrderedRing.toZeroLEOneClass`
`abs_unit_intCast` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddGroupWithOne.toIntCast` `Units.val` `Int.instMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Int.units_eq_one_or` `Int.cast_one` `abs_one` `Int.cast_neg` `abs_neg`
`abs_zsmul` 📖	mathematical	—	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `instLatticeInt` `Int.instAddGroup`	—	`le_total` `natCast_zsmul` `abs_nsmul` `Nat.abs_cast` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `neg_nonneg` `Int.instAddLeftMono` `abs_neg` `neg_zsmul`
`dvd_abs` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_choice`
`exists_abs_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`lt_of_lt_of_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `lt_add_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`le_of_sq_le_sq` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—	`LE.le.trans` `le_abs_self` `abs_le_of_sq_le_sq`
`mabs_zpow` 📖	mathematical	—	`mabs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CommGroup.toGroup` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `abs` `instLatticeInt` `Int.instAddGroup`	—	`le_total` `zpow_natCast` `mabs_pow` `Nat.abs_cast` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `neg_nonneg` `Int.instAddLeftMono` `mabs_inv` `zpow_neg` `abs_neg`
`odd_abs` 📖	mathematical	—	`Odd` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_choice`
`one_le_sq_iff_one_le_abs` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `AddGroupWithOne.toAddGroup`	—	`one_pow` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `sq_le_sq`
`one_lt_sq_iff_one_lt_abs` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `AddGroupWithOne.toAddGroup`	—	`one_pow` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `sq_lt_sq`
`pow_abs` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`abs_pow`
`pow_eq_neg_one_iff` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Odd` `Nat.instSemiring`	—	`one_pow` `pow_eq_neg_pow_iff` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`pow_eq_neg_pow_iff` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Odd` `Nat.instSemiring`	—	`Nat.even_or_odd` `lt_of_lt_of_le` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Even.pow_pos` `AddGroup.existsAddOfLE` `Even.pow_nonneg` `Nat.not_odd_iff_even` `LT.lt.ne'` `Odd.neg_pow` `StrictMono.injective` `Odd.strictMono_pow`
`pow_eq_one_iff_cases` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Even`	—	`one_pow`
`pow_eq_one_iff_of_ne_zero` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Even`	—	`pow_eq_pow_iff_of_ne_zero` `one_pow`
`pow_eq_pow_iff_cases` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Even`	—	`eq_or_ne` `pow_zero`
`pow_eq_pow_iff_of_ne_zero` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Even`	—	`Nat.even_xor_odd` `pow_left_inj₀` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Even.pow_abs` `StrictMono.injective` `Odd.strictMono_pow` `AddGroup.existsAddOfLE`
`self_dvd_abs` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`dvd_abs` `dvd_refl`
`sq_abs` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sq` `abs_mul_abs_self`
`sq_eq_sq_iff_abs_eq_abs` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	—
`sq_le_one_iff_abs_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `abs` `AddGroupWithOne.toAddGroup`	—	`one_pow` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `sq_le_sq`
`sq_le_sq` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sq_abs` `sq_le_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`sq_le_sq'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`sq_le_sq` `le_trans` `abs_le` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `le_abs_self`
`sq_lt_one_iff_abs_lt_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `abs` `AddGroupWithOne.toAddGroup`	—	`one_pow` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `sq_lt_sq`
`sq_lt_sq` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sq_abs` `sq_lt_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`sq_lt_sq'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`sq_lt_sq` `lt_of_lt_of_le` `abs_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `le_abs_self`

---

← Back to Index