Documentation Verification Report

Units

📁 Source: Mathlib/Data/ZMod/Units.lean

Statistics

Metric	Count
Definitions `unitOfIsCoprime`, `unitsMap`	2
Theorems `coe_int_inv_mul_eq_one`, `coe_int_mul_inv_eq_one`, `coe_int_mul_val_inv`, `coe_int_val_inv_mul`, `coe_unitOfIsCoprime`, `eq_unit_mul_divisor`, `isUnit_cast_of_dvd`, `isUnit_inv`, `not_isUnit_of_mem_primeFactors`, `unitsMap_comp`, `unitsMap_def`, `unitsMap_self`, `unitsMap_surjective`, `unitsMap_val`	14
Total	16

ZMod

Definitions

Name	Category	Theorems
`unitOfIsCoprime` 📖	CompOp	1 math math: `coe_unitOfIsCoprime`
`unitsMap` 📖	CompOp	9 math math: `unitsMap_surjective`, `DirichletCharacter.changeLevel_def`, `unitsMap_self`, `DirichletCharacter.changeLevel_toUnitHom`, `unitsMap_comp`, `IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply`, `unitsMap_val`, `DirichletCharacter.factorsThrough_iff_ker_unitsMap`, `unitsMap_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_int_inv_mul_eq_one` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `instInv` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`mul_comm` `coe_int_mul_inv_eq_one`
`coe_int_mul_inv_eq_one` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `instInv` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Int.isUnit_eq_one_or` `Nat.cast_zero` `Int.cast_one` `inv_one` `mul_one` `Int.cast_neg` `inv_neg_one` `mul_neg` `neg_neg` `natCast_zmod_val` `coe_mul_inv_eq_one` `val_intCast` `Int.gcd_emod` `Int.isCoprime_iff_gcd_eq_one`
`coe_int_mul_val_inv` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `val` `instInv` `AddMonoidWithOne.toOne`	—	`natCast_zmod_val` `coe_int_mul_inv_eq_one`
`coe_int_val_inv_mul` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `val` `instInv` `AddGroupWithOne.toIntCast` `AddMonoidWithOne.toOne`	—	`mul_comm` `coe_int_mul_val_inv`
`coe_unitOfIsCoprime` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`Units.val` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `unitOfIsCoprime` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`eq_unit_mul_divisor` 📖	mathematical	—	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`eq_or_ne` `dvd_zero` `isUnit_one` `Nat.cast_zero` `MulZeroClass.mul_zero` `lt_or_gt_of_ne` `isUnit_iff_coprime` `Nat.isCoprime_iff_coprime` `Nat.gcd_eq_gcd_ab` `Nat.cast_ne_zero` `Int.instCharZero` `mul_comm` `mul_add` `Distrib.leftDistribClass` `mul_assoc` `Nat.cast_mul` `unitsMap_surjective` `Units.isUnit` `natCast_zmod_val` `natCast_eq_natCast_iff` `Nat.ModEq.eq_1` `charP` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MonoidHom.coe_coe` `IsUnit.unit_spec` `Units.coe_map` `unitsMap_def` `natCast_val` `castHom_apply`
`isUnit_cast_of_dvd` 📖	mathematical	—	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `cast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Units.val`	—	`Units.isUnit`
`isUnit_inv` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	`instInv`	—	`isUnit_iff_exists` `inv_mul_of_unit` `mul_inv_of_unit`
`not_isUnit_of_mem_primeFactors` 📖	mathematical	`Finset` `Finset.instMembership` `Nat.primeFactors`	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`isUnit_iff_coprime` `Nat.Prime.dvd_iff_not_coprime` `Nat.prime_of_mem_primeFactors` `Nat.dvd_of_mem_primeFactors`
`unitsMap_comp` 📖	mathematical	—	`MonoidHom.comp` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `MulOneClass.toMulOne` `Units.instMulOneClass` `unitsMap` `dvd_trans` `Nat.instSemigroup`	—	`dvd_trans` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `charP` `Units.map_comp` `castHom_comp`
`unitsMap_def` 📖	mathematical	—	`unitsMap` `Units.map` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `MonoidHomClass.toMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `NonAssocSemiring.toMulZeroOneClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `castHom` `charP`	—	—
`unitsMap_self` 📖	mathematical	—	`unitsMap` `dvd_refl` `Nat.instMonoid` `MonoidHom.id` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `MulOneClass.toMulOne` `Units.instMulOneClass`	—	`dvd_refl` `charP` `MonoidHomClass.toMonoidHom.congr_simp` `castHom_self` `Units.map_id`
`unitsMap_surjective` 📖	mathematical	—	`Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `unitsMap`	—	`Nat.coprime_of_dvd` `Nat.Prime.dvd_mul` `add_comm` `Prime.dvd_finset_prod_iff` `Nat.Prime.prime` `Nat.prime_dvd_prime_iff_eq` `Nat.mem_primeFactors` `Finset.mem_filter` `Nat.Prime.not_coprime_iff_dvd` `Dvd.dvd.mul_right` `Finset.dvd_prod_of_mem` `val_coe_unit_coprime` `Units.ext` `eq_zero_of_zero_dvd` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `charP` `Nat.cast_add` `natCast_val` `Nat.cast_mul` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `ringHom_map_cast` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_natCast` `CharP.cast_eq_zero` `MulZeroClass.mul_zero` `add_zero`
`unitsMap_val` 📖	mathematical	—	`Units.val` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `unitsMap` `cast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—

---

← Back to Index