Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `castHom`, `signHom`	2
Theorems `castHom_apply`, `coe_mul`, `coe_pow`, `coe_zpow`, `intCast_cast`, `pow_even`, `pow_odd`, `range_eq`, `univ_eq`, `zpow_even`, `zpow_odd`, `abs_mul_sign`, `exists_signed_sum`, `exists_signed_sum'`, `self_mul_sign`, `signHom_apply`, `sign_intCast`, `sign_mul`, `sign_mul_abs`, `sign_mul_self`, `sign_pow`, `sign_sum`	22
Total	24

SignType

Definitions

Name	Category	Theorems
`castHom` 📖	CompOp	1 math math: `castHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `SignType` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `instCommGroupWithZero` `MonoidWithZeroHom.funLike` `castHom` `cast` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass`	—	—
`coe_mul` 📖	mathematical	—	`cast` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SignType` `instMul` `MulZeroClass.toMul`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`coe_pow` 📖	mathematical	—	`cast` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SignType` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `instCommGroupWithZero`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`coe_zpow` 📖	mathematical	—	`cast` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SignType` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `instCommGroupWithZero`	—	`map_zpow₀` `MonoidWithZeroHom.monoidWithZeroHomClass`
`intCast_cast` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `cast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup` `NegZeroClass.toNeg`	—	`map_cast'` `Int.cast_one` `Int.cast_zero` `Int.cast_neg`
`pow_even` 📖	mathematical	`Even`	`SignType` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `instCommGroupWithZero` `instOne`	—	`Even.neg_pow` `one_pow`
`pow_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`SignType` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `instCommGroupWithZero`	—	`pow_add` `pow_one` `pow_mul` `sq` `MulZeroClass.mul_zero` `mul_neg` `mul_one` `neg_neg` `one_pow`
`range_eq` 📖	mathematical	—	`Set.range` `SignType` `Set` `Set.instInsert` `zero` `neg` `Set.instSingletonSet` `pos`	—	`Fintype.coe_image_univ` `univ_eq` `Finset.image_insert` `Finset.image_singleton` `Finset.coe_insert` `Finset.coe_singleton`
`univ_eq` 📖	mathematical	—	`Finset.univ` `SignType` `instFintypeSignType` `Finset` `Finset.instInsert` `instDecidableEqSignType` `instZero` `instNeg` `instOne` `Finset.instSingleton`	—	—
`zpow_even` 📖	mathematical	`Even`	`SignType` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `instCommGroupWithZero` `instOne`	—	`Even.neg_one_zpow` `one_zpow`
`zpow_odd` 📖	mathematical	`Odd` `Int.instSemiring`	`SignType` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `instCommGroupWithZero`	—	`eq_or_ne` `zero_zpow` `zpow_add₀` `zpow_one` `zpow_mul` `zpow_two` `MulZeroClass.mul_zero` `mul_neg` `mul_one` `neg_neg` `one_zpow`

(root)

Definitions

Name	Category	Theorems
`signHom` 📖	CompOp	1 math math: `signHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_mul_sign` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `SignType.cast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `LinearOrder.toDecidableLT`	—	`lt_trichotomy` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sign_neg` `SignType.coe_neg` `mul_neg` `mul_one` `neg_neg` `abs_zero` `sign_zero` `MulZeroClass.mul_zero` `abs_of_pos` `sign_pos`
`exists_signed_sum` 📖	mathematical	—	`Finset` `Finset.instMembership` `Fintype.card` `Finset.sum` `Nat.instAddCommMonoid` `Int.instAddCommMonoid` `Finset.univ` `SignType.cast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	—	`Fintype.card_coe` `Finset.sum_attach`
`exists_signed_sum'` 📖	mathematical	`Finset.sum` `Nat.instAddCommMonoid`	`SignType` `SignType.instZero` `Fintype.card` `Int.instAddCommMonoid` `Finset.univ` `SignType.cast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	—	`exists_signed_sum` `Fintype.card_sum` `Fintype.card_fin` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Fintype.sum_sum_type` `Finset.sum_congr` `Finset.sum_const_zero` `add_zero`
`self_mul_sign` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SignType.cast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `LinearOrder.toDecidableLT` `abs` `AddGroupWithOne.toAddGroup`	—	`lt_trichotomy` `sign_neg` `SignType.coe_neg` `mul_neg` `mul_one` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sign_zero` `MulZeroClass.mul_zero` `abs_zero` `sign_pos` `abs_of_pos`
`signHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `SignType` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `SignType.instCommGroupWithZero` `MonoidWithZeroHom.funLike` `signHom` `OrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `LinearOrder.toDecidableLT`	—	—
`sign_intCast` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `instLatticeInt` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `NeZero.one`
`sign_mul` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearOrder.toDecidableLT` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SignType.instMul`	—	`lt_trichotomy` `sign_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `sign_neg` `mul_neg` `mul_one` `neg_neg` `MulZeroClass.mul_zero` `sign_zero` `MulZeroClass.zero_mul` `neg_zero` `IsStrictOrderedRing.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE`
`sign_mul_abs` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SignType.cast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `LinearOrder.toDecidableLT` `abs` `AddGroupWithOne.toAddGroup`	—	`lt_trichotomy` `sign_neg` `SignType.coe_neg` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `mul_neg` `neg_mul` `one_mul` `neg_neg` `sign_zero` `abs_zero` `MulZeroClass.mul_zero` `sign_pos` `abs_of_pos`
`sign_mul_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SignType.cast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `LinearOrder.toDecidableLT` `abs` `AddGroupWithOne.toAddGroup`	—	`lt_trichotomy` `sign_neg` `SignType.coe_neg` `neg_mul` `one_mul` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sign_zero` `MulZeroClass.mul_zero` `abs_zero` `sign_pos` `abs_of_pos`
`sign_pow` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearOrder.toDecidableLT` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `SignType.instCommGroupWithZero`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`sign_sum` 📖	mathematical	`Finset.Nonempty` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearOrder.toDecidableLT`	`Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`Finset.sum_eq_zero` `Finset.sum_neg` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `Finset.sum_pos`

---

← Back to Index