Documentation Verification Report

UInt

📁 Source: Mathlib/Data/UInt.lean

Statistics

Metric	Count
Definitions `instCommMonoid`, `instCommRing`, `instNonUnitalCommRing`, `instCommMonoid`, `instCommRing`, `instNonUnitalCommRing`, `instCommMonoid`, `instCommRing`, `instNonUnitalCommRing`, `instCommMonoid`, `instCommRing`, `instNonUnitalCommRing`, `isASCIIAlpha`, `isASCIIAlphanum`, `isASCIIDigit`, `isASCIILower`, `isASCIIUpper`, `toChar`, `instCommMonoid`, `instCommRing`, `instNonUnitalCommRing`	21
Theorems `toBitVec_injective`, `toBitVec_intCast`, `toBitVec_natCast`, `toBitVec_nsmul`, `toBitVec_zsmul`, `toFin_injective`, `toBitVec_injective`, `toBitVec_intCast`, `toBitVec_natCast`, `toBitVec_nsmul`, `toBitVec_zsmul`, `toFin_injective`, `toBitVec_injective`, `toBitVec_intCast`, `toBitVec_natCast`, `toBitVec_nsmul`, `toBitVec_zsmul`, `toFin_injective`, `toBitVec_injective`, `toBitVec_intCast`, `toBitVec_natCast`, `toBitVec_nsmul`, `toBitVec_zsmul`, `toFin_injective`, `toBitVec_injective`, `toBitVec_intCast`, `toBitVec_natCast`, `toBitVec_nsmul`, `toBitVec_zsmul`, `toFin_injective`	30
Total	51

UInt16

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBitVec_injective` 📖	—	—	—	—	—
`toBitVec_intCast` 📖	—	—	—	—	`Int.cast_neg` `Int.cast_natCast`
`toBitVec_natCast` 📖	—	—	—	—	—
`toBitVec_nsmul` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`nsmul_eq_mul`
`toBitVec_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`toBitVec_intCast`
`toFin_injective` 📖	—	—	—	—	—

UInt32

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBitVec_injective` 📖	—	—	—	—	—
`toBitVec_intCast` 📖	—	—	—	—	`Int.cast_neg` `Int.cast_natCast`
`toBitVec_natCast` 📖	—	—	—	—	—
`toBitVec_nsmul` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`nsmul_eq_mul`
`toBitVec_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`toBitVec_intCast`
`toFin_injective` 📖	—	—	—	—	—

UInt64

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBitVec_injective` 📖	—	—	—	—	—
`toBitVec_intCast` 📖	—	—	—	—	`Int.cast_neg` `Int.cast_natCast`
`toBitVec_natCast` 📖	—	—	—	—	—
`toBitVec_nsmul` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`nsmul_eq_mul`
`toBitVec_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`toBitVec_intCast`
`toFin_injective` 📖	—	—	—	—	—

UInt8

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—
`isASCIIAlpha` 📖	CompOp	—
`isASCIIAlphanum` 📖	CompOp	—
`isASCIIDigit` 📖	CompOp	—
`isASCIILower` 📖	CompOp	—
`isASCIIUpper` 📖	CompOp	—
`toChar` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBitVec_injective` 📖	—	—	—	—	—
`toBitVec_intCast` 📖	—	—	—	—	`Int.cast_neg` `Int.cast_natCast`
`toBitVec_natCast` 📖	—	—	—	—	—
`toBitVec_nsmul` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`nsmul_eq_mul`
`toBitVec_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`toBitVec_intCast`
`toFin_injective` 📖	—	—	—	—	—

USize

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBitVec_injective` 📖	—	—	—	—	—
`toBitVec_intCast` 📖	—	—	—	—	`Int.cast_neg` `Int.cast_natCast`
`toBitVec_natCast` 📖	—	—	—	—	—
`toBitVec_nsmul` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`nsmul_eq_mul`
`toBitVec_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `BitVec.instCommRing`	—	`toBitVec_intCast`
`toFin_injective` 📖	—	—	—	—	—

---

← Back to Index