Documentation Verification Report

BitVec

📁 Source: Mathlib/Data/BitVec.lean

Statistics

Metric	Count
Definitions `equivFin`, `instCommRing`, `instCommSemiring`	3
Theorems `equivFin_apply`, `equivFin_symm_apply_toFin`, `ofFin_intCast`, `toFin_injective`, `toFin_intCast`, `toFin_nsmul`, `toFin_pow`, `toFin_zsmul`, `toNat_injective`	9
Total	12

BitVec

Definitions

Name	Category	Theorems
`equivFin` 📖	CompOp	2 math math: `equivFin_symm_apply_toFin`, `equivFin_apply`
`instCommRing` 📖	CompOp	10 math math: `UInt8.toBitVec_zsmul`, `UInt64.toBitVec_zsmul`, `UInt16.toBitVec_nsmul`, `USize.toBitVec_zsmul`, `UInt64.toBitVec_nsmul`, `UInt32.toBitVec_nsmul`, `UInt8.toBitVec_nsmul`, `UInt16.toBitVec_zsmul`, `UInt32.toBitVec_zsmul`, `USize.toBitVec_nsmul`
`instCommSemiring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivFin_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Monoid.toNatPow` `Nat.instMonoid` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivFin`	—	—
`equivFin_symm_apply_toFin` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Monoid.toNatPow` `Nat.instMonoid` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equivFin`	—	—
`ofFin_intCast` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Fin.instCommRing`	—	`Fin.val_intCast` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_ofNat` `Nat.cast_pow`
`toFin_injective` 📖	—	—	—	—	—
`toFin_intCast` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Fin.instCommRing`	—	`ofFin_intCast`
`toFin_nsmul` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `Fin.instAddMonoidWithOne`	—	`nsmul_eq_mul`
`toFin_pow` 📖	—	—	—	—	`Nat.cast_one` `pow_zero` `pow_succ`
`toFin_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Fin.addCommGroup`	—	`toFin_intCast` `zsmul_eq_mul`
`toNat_injective` 📖	—	—	—	—	—

---

← Back to Index