Documentation Verification Report

Invertible

📁 Source: Mathlib/Algebra/CharP/Invertible.lean

Statistics

Metric	Count
Definitions `invertibleOfCharPNotDvd`, `invertibleOfCoprime`, `invertibleOfPos`, `invertibleOfRingCharNotDvd`, `invertibleSucc`, `invertibleThree`, `invertibleTwo`	7
Theorems `intCast_mul_natCast_gcdA_eq_gcd`, `isUnit_intCast_iff`, `isUnit_natCast_iff`, `isUnit_ofNat_iff`, `natCast_gcdA_mul_intCast_eq_gcd`, `all`, `all`, `invOf_eq_of_coprime`, `not_ringChar_dvd_of_invertible`	9
Total	16

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast_mul_natCast_gcdA_eq_gcd` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddGroupWithOne.toIntCast` `Nat.gcdA`	—	`Nat.gcd_eq_gcd_ab` `Int.cast_add` `Int.cast_mul` `Int.cast_natCast` `cast_eq_zero` `MulZeroClass.zero_mul` `add_zero`
`isUnit_intCast_iff` 📖	mathematical	`Nat.Prime`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`Int.cast_natCast` `isUnit_natCast_iff` `Int.cast_neg`
`isUnit_natCast_iff` 📖	mathematical	`Nat.Prime`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`nontrivial_of_char_ne_one` `Nat.Prime.ne_one` `cast_eq_zero_iff` `IsUnit.ne_zero` `isUnit_of_invertible` `Nat.Prime.coprime_iff_not_dvd`
`isUnit_ofNat_iff` 📖	mathematical	`Nat.Prime`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`isUnit_natCast_iff`
`natCast_gcdA_mul_intCast_eq_gcd` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Nat.gcdA` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`Commute.eq` `Nat.commute_cast` `intCast_mul_natCast_gcdA_eq_gcd`

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all` 📖	mathematical	—	`Even` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `of_isUnit_two` `isUnit_of_invertible`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all` 📖	mathematical	—	`Odd` `Ring.toSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `of_isUnit_two` `isUnit_of_invertible`

(root)

Definitions

Name	Category	Theorems
`invertibleOfCharPNotDvd` 📖	CompOp	—
`invertibleOfCoprime` 📖	CompOp	—
`invertibleOfPos` 📖	CompOp	2 math math: `xInTermsOfW_vars_subset`, `xInTermsOfW_vars_aux`
`invertibleOfRingCharNotDvd` 📖	CompOp	—
`invertibleSucc` 📖	CompOp	—
`invertibleThree` 📖	CompOp	—
`invertibleTwo` 📖	CompOp	42 math math: `EuclideanGeometry.Sphere.isDiameter_iff_right_mem_and_midpoint_eq_center`, `AffineSubspace.mem_perpBisector_iff_inner_eq_zero'`, `QuadraticForm.posDef_toMatrix'`, `sbtw_midpoint_of_ne`, `lineMap_inv_two`, `IsometryEquiv.midpoint_fixed`, `AffineIsometryEquiv.pointReflection_midpoint_left`, `EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint`, `EuclideanGeometry.oangle_midpoint_right`, `AffineSubspace.mem_perpBisector_iff_inner_eq_zero`, `EuclideanGeometry.oangle_midpoint_rev_left`, `EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center`, `midpoint_le_right`, `dist_midpoint_midpoint_le`, `IsometryEquiv.map_midpoint`, `Affine.Triangle.circumsphere_eq_of_dist_of_oangle`, `EuclideanGeometry.oangle_midpoint_left`, `midpoint_le_left`, `EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center`, `imaginaryPart_eq_neg_I_smul_skewAdjointPart`, `Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter`, `AffineSubspace.midpoint_mem_perpBisector`, `nndist_midpoint_midpoint_le`, `EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq`, `Affine.Triangle.eulerPoint_eq_midpoint`, `Affine.Simplex.midpoint_faceOppositeCentroid_eulerPoint`, `EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center`, `EuclideanGeometry.oangle_midpoint_rev_right`, `lineMap_one_half`, `EuclideanGeometry.angle_midpoint_eq_pi`, `left_le_midpoint`, `skewAdjointPart_eq_I_smul_imaginaryPart`, `EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq`, `right_le_midpoint`, `EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq`, `homothety_inv_two`, `EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_midpoint_eq_center`, `wbtw_midpoint`, `eq_midpoint_of_dist_eq_half`, `homothety_one_half`, `AffineIsometryEquiv.pointReflection_midpoint_right`, `Urysohns.CU.lim_eq_midpoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`invOf_eq_of_coprime` 📖	mathematical	—	`Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toIntCast` `Nat.gcdA`	—	`Invertible.congr`
`not_ringChar_dvd_of_invertible` 📖	mathematical	—	`ringChar` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`ringChar.spec` `Invertible.ne_zero`

---

← Back to Index