Documentation Verification Report

Nat

📁 Source: Mathlib/Algebra/Order/Antidiag/Nat.lean

Statistics

Metric	Count
Definitions `finMulAntidiag`, `instHasAntidiagonal`	2
Theorems `card_finMulAntidiag_of_squarefree`, `card_pair_lcm_eq`, `dvd_of_mem_finMulAntidiag`, `finMulAntidiag_eq_piFinset_divisors_filter`, `finMulAntidiag_existsUnique_prime_dvd`, `finMulAntidiag_one`, `finMulAntidiag_three`, `finMulAntidiag_zero_left`, `finMulAntidiag_zero_right`, `image_apply_finMulAntidiag`, `image_piFinTwoEquiv_finMulAntidiag`, `mem_finMulAntidiag`, `ne_zero_of_mem_finMulAntidiag`, `prod_eq_of_mem_finMulAntidiag`	14
Total	16

Nat

Definitions

Name	Category	Theorems
`finMulAntidiag` 📖	CompOp	8 math math: `finMulAntidiag_zero_right`, `mem_finMulAntidiag`, `finMulAntidiag_one`, `image_piFinTwoEquiv_finMulAntidiag`, `image_apply_finMulAntidiag`, `finMulAntidiag_zero_left`, `finMulAntidiag_eq_piFinset_divisors_filter`, `card_finMulAntidiag_of_squarefree`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_finMulAntidiag_of_squarefree` 📖	mathematical	`Squarefree` `instMonoid`	`Finset.card` `finMulAntidiag` `Monoid.toNatPow` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `instMulZeroClass` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.cardDistinctFactors`	—	`Finset.card_pi` `Finset.prod_const` `ArithmeticFunction.cardDistinctFactors_apply` `List.card_toFinset` `toFinset_factors` `Finset.card_fin`
`card_pair_lcm_eq` 📖	mathematical	`Squarefree` `instMonoid`	`Finset.card` `Finset.filter` `SProd.sprod` `Finset` `Finset.instSProd` `divisors` `Monoid.toNatPow` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `instMulZeroClass` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.cardDistinctFactors`	—	`card_finMulAntidiag_of_squarefree` `Finset.card_bij` `Squarefree.ne_zero` `instNontrivial`
`dvd_of_mem_finMulAntidiag` 📖	—	`Finset` `Finset.instMembership` `finMulAntidiag`	—	—	`mem_finMulAntidiag` `Finset.dvd_prod_of_mem` `Finset.mem_univ`
`finMulAntidiag_eq_piFinset_divisors_filter` 📖	mathematical	—	`finMulAntidiag` `Finset.filter` `Finset.prod` `instCommMonoid` `Finset.univ` `Fin.fintype` `Fintype.piFinset` `divisors`	—	`Finset.ext` `Dvd.dvd.trans` `dvd_of_mem_finMulAntidiag` `prod_eq_of_mem_finMulAntidiag` `mem_finMulAntidiag` `ne_zero_of_dvd_ne_zero`
`finMulAntidiag_existsUnique_prime_dvd` 📖	mathematical	`Squarefree` `instMonoid` `primeFactorsList` `Finset` `Finset.instMembership` `finMulAntidiag`	`ExistsUnique`	—	`Prime.dvd_finset_prod_iff` `Prime.prime` `mem_finMulAntidiag` `mem_primeFactorsList` `Prime.not_coprime_iff_dvd` `coprime_of_squarefree_mul` `Squarefree.squarefree_of_dvd` `Finset.mul_prod_erase` `Finset.mem_erase` `Finset.mem_univ` `mul_assoc`
`finMulAntidiag_one` 📖	mathematical	—	`finMulAntidiag` `Finset` `Finset.instSingleton`	—	`Finset.ext` `Unique.instSubsingleton`
`finMulAntidiag_three` 📖	—	`Finset` `Finset.instMembership` `finMulAntidiag`	—	—	`mem_finMulAntidiag` `Fin.prod_univ_three`
`finMulAntidiag_zero_left` 📖	mathematical	—	`finMulAntidiag` `Finset` `Finset.instEmptyCollection`	—	`Finset.ext` `Finset.prod_congr` `Finset.univ_eq_empty` `Fin.isEmpty'`
`finMulAntidiag_zero_right` 📖	mathematical	—	`finMulAntidiag` `Finset` `Finset.instEmptyCollection`	—	—
`image_apply_finMulAntidiag` 📖	mathematical	—	`Finset.image` `finMulAntidiag` `divisors`	—	`Finset.ext` `dvd_of_mem_finMulAntidiag` `mem_finMulAntidiag` `Fin.nontrivial_iff_two_le` `eq_or_ne` `exists_ne` `Finset.prod_congr` `Finset.mul_prod_erase` `Finset.mem_univ` `Finset.mem_erase` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `Unique.instSubsingleton`
`image_piFinTwoEquiv_finMulAntidiag` 📖	mathematical	—	`Finset.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `piFinTwoEquiv` `finMulAntidiag` `divisorsAntidiagonal`	—	`Finset.ext` `Fin.prod_univ_two` `Function.Surjective.exists` `Equiv.surjective` `Fin.cons_zero` `Fin.cons_one`
`mem_finMulAntidiag` 📖	mathematical	—	`Finset` `Finset.instMembership` `finMulAntidiag` `Finset.prod` `instCommMonoid` `Finset.univ` `Fin.fintype`	—	`PNat.coe_injective` `Equiv.symm_apply_eq` `Function.Surjective.exists` `Equiv.surjective` `Finset.prod_congr` `Finset.PNat.coe_prod` `LT.lt.ne` `Finset.prod_ne_zero_iff` `instNontrivial` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `Finset.mem_univ`
`ne_zero_of_mem_finMulAntidiag` 📖	—	`Finset` `Finset.instMembership` `finMulAntidiag`	—	—	`ne_zero_of_dvd_ne_zero` `mem_finMulAntidiag` `dvd_of_mem_finMulAntidiag`
`prod_eq_of_mem_finMulAntidiag` 📖	mathematical	`Finset` `Finset.instMembership` `finMulAntidiag`	`Finset.prod` `instCommMonoid` `Finset.univ` `Fin.fintype`	—	`mem_finMulAntidiag`

PNat

Definitions

Name	Category	Theorems
`instHasAntidiagonal` 📖	CompOp	—

---

← Back to Index