Documentation Verification Report

Prod

📁 Source: Mathlib/Data/Finite/Prod.lean

Statistics

Metric	Count
Definitions `fintypeImage2`, `fintypeOffDiag`, `fintypeProd`	3
Theorems `finite_left`, `finite_right`, `finite_left`, `finite_right`, `finite_image2`, `finite_prod`, `instPProd`, `instProd`, `prod_left`, `prod_right`, `finite`, `finite_left`, `finite_right`, `finite`, `finite_iff`, `image2`, `of_prod_left`, `of_prod_right`, `offDiag`, `prod`, `toFinset_offDiag`, `toFinset_prod`, `image2_left`, `image2_right`, `prod_left`, `prod_right`, `finite_image2`, `finite_image_fst_and_snd_iff`, `finite_prod`, `infinite_image2`, `infinite_prod`	31
Total	34

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_left` 📖	mathematical	—	`Finite` `AddEquiv`	—	`Finite.of_injective` `Equiv.finite_left` `toEquiv_injective`
`finite_right` 📖	mathematical	—	`Finite` `AddEquiv`	—	`Finite.of_injective` `Equiv.finite_right` `toEquiv_injective`

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_left` 📖	mathematical	—	`Finite` `Equiv`	—	`Finite.of_equiv` `finite_right` `symm_symm`
`finite_right` 📖	mathematical	—	`Finite` `Equiv`	—	`Finite.of_injective` `Function.Embedding.finite` `ext` `DFunLike.congr_fun`

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPProd` 📖	mathematical	—	`Finite`	—	`of_equiv` `instProd` `instFinitePLift`
`instProd` 📖	mathematical	—	`Finite`	—	`of_fintype`
`prod_left` 📖	mathematical	—	`Finite`	—	`of_surjective` `Prod.fst_surjective`
`prod_right` 📖	mathematical	—	`Finite`	—	`of_surjective` `Prod.snd_surjective`

Finite.Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_image2` 📖	mathematical	—	`Finite` `Set.Elem` `Set.image2`	—	`Set.image_prod` `finite_image` `finite_prod`
`finite_prod` 📖	mathematical	—	`Finite` `Set.Elem` `SProd.sprod` `Set` `Set.instSProd`	—	`Finite.of_equiv` `Finite.instProd`

Function.Embedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite` `Function.Embedding`	—	`isEmpty_or_nonempty` `Finite.of_subsingleton` `IsEmpty.instSubsingleton` `Finite.of_injective` `Pi.finite` `injective` `DFunLike.coe_injective`

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_left` 📖	mathematical	—	`Finite` `MulEquiv`	—	`Finite.of_injective` `Equiv.finite_left` `toEquiv_injective`
`finite_right` 📖	mathematical	—	`Finite` `MulEquiv`	—	`Finite.of_injective` `Equiv.finite_right` `toEquiv_injective`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	—	`Finite`	—	—	`Finite.of_equiv` `Finite.of_fintype` `instFinitePLift`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff` 📖	mathematical	—	`Finite`	—	`Finite.prod_left` `Finite.prod_right` `Finite.instProd`

Set

Definitions

Name	Category	Theorems
`fintypeImage2` 📖	CompOp	—
`fintypeOffDiag` 📖	CompOp	3 math math: `einfsep_of_fintype`, `Nontrivial.infsep_of_fintype`, `infsep_of_fintype`
`fintypeProd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_image2` 📖	mathematical	`InjOn`	`Finite` `image2` `Set` `instEmptyCollection`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_and_or_eq` `infinite_image2`
`finite_image_fst_and_snd_iff` 📖	mathematical	—	`Finite` `image`	—	`Finite.subset` `Finite.prod` `mem_image_of_mem` `Finite.image`
`finite_prod` 📖	mathematical	—	`Finite` `SProd.sprod` `Set` `instSProd` `instEmptyCollection`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_and_or_eq` `infinite_prod`
`infinite_image2` 📖	mathematical	`InjOn`	`Infinite` `image2` `Nonempty`	—	`infinite_prod` `Infinite.of_image` `image_uncurry_prod` `Infinite.image2_left` `Infinite.image2_right`
`infinite_prod` 📖	mathematical	—	`Infinite` `SProd.sprod` `Set` `instSProd` `Nonempty`	—	`Finite.prod` `Nonempty.snd` `Infinite.nonempty` `Nonempty.fst` `Infinite.prod_left` `Infinite.prod_right`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image2` 📖	mathematical	—	`Set.Finite` `Set.image2`	—	`to_subtype` `Set.toFinite` `Finite.Set.finite_image2`
`of_prod_left` 📖	mathematical	`Set.Nonempty`	`Set.Finite`	—	`subset` `image`
`of_prod_right` 📖	mathematical	`Set.Nonempty`	`Set.Finite`	—	`subset` `image`
`offDiag` 📖	mathematical	—	`Set.Finite` `Set.offDiag`	—	`subset` `prod` `Set.offDiag_subset_prod`
`prod` 📖	mathematical	—	`Set.Finite` `SProd.sprod` `Set` `Set.instSProd`	—	`to_subtype` `Set.toFinite` `Finite.Set.finite_prod`
`toFinset_offDiag` 📖	mathematical	—	`toFinset` `Set.offDiag` `offDiag` `Finset.offDiag`	—	`Finset.ext` `offDiag`
`toFinset_prod` 📖	mathematical	—	`SProd.sprod` `Finset` `Finset.instSProd` `toFinset` `Set` `Set.instSProd` `prod`	—	`Finset.ext` `prod`

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image2_left` 📖	mathematical	`Set.Infinite` `Set` `Set.instMembership` `Set.InjOn`	`Set.image2`	—	`mono` `Set.image_subset_image2_left` `image`
`image2_right` 📖	mathematical	`Set.Infinite` `Set` `Set.instMembership` `Set.InjOn`	`Set.image2`	—	`mono` `Set.image_subset_image2_right` `image`
`prod_left` 📖	mathematical	`Set.Infinite` `Set.Nonempty`	`SProd.sprod` `Set` `Set.instSProd`	—	`Set.Finite.of_prod_left`
`prod_right` 📖	mathematical	`Set.Infinite` `Set.Nonempty`	`SProd.sprod` `Set` `Set.instSProd`	—	`Set.Finite.of_prod_right`

---

← Back to Index