Documentation Verification Report

Sign

📁 Source: Mathlib/Data/Real/Sign.lean

Statistics

Metric	Count
Definitions `sign`	1
Theorems `inv_sign`, `sign_apply_eq`, `sign_apply_eq_of_ne_zero`, `sign_eq_zero_iff`, `sign_intCast`, `sign_inv`, `sign_mul_nonneg`, `sign_mul_pos_of_ne_zero`, `sign_neg`, `sign_of_neg`, `sign_of_pos`, `sign_one`, `sign_zero`	13
Total	14

Real

Definitions

Name	Category	Theorems
`sign` 📖	CompOp	13 math math: `sign_one`, `sign_inv`, `sign_zero`, `sign_eq_zero_iff`, `sign_mul_nonneg`, `sign_of_pos`, `sign_neg`, `sign_mul_pos_of_ne_zero`, `sign_apply_eq`, `inv_sign`, `sign_apply_eq_of_ne_zero`, `sign_of_neg`, `sign_intCast`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_sign` 📖	mathematical	—	`Real` `instInv` `sign`	—	`sign_apply_eq` `inv_neg` `inv_one` `inv_zero`
`sign_apply_eq` 📖	mathematical	—	`sign` `Real` `instNeg` `instOne` `instZero`	—	`lt_trichotomy` `sign_of_neg` `sign_zero` `sign_of_pos`
`sign_apply_eq_of_ne_zero` 📖	mathematical	—	`sign` `Real` `instNeg` `instOne`	—	`sign_of_neg` `sign_of_pos` `Ne.lt_or_gt`
`sign_eq_zero_iff` 📖	mathematical	—	`sign` `Real` `instZero`	—	`lt_trichotomy` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `neg_eq_zero` `sign_of_neg` `sign_of_pos` `sign_zero`
`sign_intCast` 📖	mathematical	—	`sign` `Real` `instIntCast`	—	`lt_trichotomy` `sign_of_neg` `Int.cast_lt_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Int.cast_neg` `Int.cast_one` `Int.cast_zero` `sign_zero` `sign_of_pos` `Int.cast_pos`
`sign_inv` 📖	mathematical	—	`sign` `Real` `instInv`	—	`lt_trichotomy` `sign_of_neg` `inv_lt_zero` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `sign_zero` `inv_zero` `sign_of_pos` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing`
`sign_mul_nonneg` 📖	mathematical	—	`Real` `instLE` `instZero` `instMul` `sign`	—	`lt_trichotomy` `sign_of_neg` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `instIsOrderedRing` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instZeroLEOneClass` `LT.lt.le` `MulZeroClass.mul_zero` `le_refl` `sign_of_pos` `one_mul`
`sign_mul_pos_of_ne_zero` 📖	mathematical	—	`Real` `instLT` `instZero` `instMul` `sign`	—	`lt_of_le_of_ne` `sign_mul_nonneg` `zero_eq_mul` `IsDomain.to_noZeroDivisors` `instIsDomain` `sign_eq_zero_iff`
`sign_neg` 📖	mathematical	—	`sign` `Real` `instNeg`	—	`lt_trichotomy` `sign_of_neg` `sign_of_pos` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `neg_neg` `sign_zero` `neg_zero` `neg_lt_zero`
`sign_of_neg` 📖	mathematical	`Real` `instLT` `instZero`	`sign` `instNeg` `instOne`	—	`sign.eq_1`
`sign_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`sign` `instOne`	—	`sign.eq_1` `LT.lt.not_gt`
`sign_one` 📖	mathematical	—	`sign` `Real` `instOne`	—	`sign_of_pos` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing`
`sign_zero` 📖	mathematical	—	`sign` `Real` `instZero`	—	`sign.eq_1` `lt_irrefl`

---

← Back to Index