Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `HasAntidiagonal`, `antidiagonalOfLocallyFinite`, `sigmaAntidiagonalEquivProd`	3
Theorems `mem_antidiagonal`, `fst_le`, `snd_le`, `antidiagonal_congr`, `antidiagonal_congr'`, `antidiagonal_subtype_ext`, `antidiagonal_subtype_ext_iff`, `antidiagonal_zero`, `filter_fst_eq_antidiagonal`, `filter_snd_eq_antidiagonal`, `hasAntidiagonal_congr`, `instSubsingletonHasAntidiagonal`, `map_prodComm_antidiagonal`, `map_swap_antidiagonal`, `sigmaAntidiagonalEquivProd_apply`, `sigmaAntidiagonalEquivProd_symm_apply_fst`, `sigmaAntidiagonalEquivProd_symm_apply_snd_coe`, `swap_mem_antidiagonal`	18
Total	21

Finset

Definitions

Name	Category	Theorems
`HasAntidiagonal` 📖	CompData	1 math math: `instSubsingletonHasAntidiagonal`
`antidiagonalOfLocallyFinite` 📖	CompOp	—
`sigmaAntidiagonalEquivProd` 📖	CompOp	3 math math: `sigmaAntidiagonalEquivProd_symm_apply_snd_coe`, `sigmaAntidiagonalEquivProd_apply`, `sigmaAntidiagonalEquivProd_symm_apply_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antidiagonal_congr` 📖	—	`Finset` `instMembership` `HasAntidiagonal.antidiagonal` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid`	—	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `HasAntidiagonal.mem_antidiagonal`
`antidiagonal_congr'` 📖	—	`Finset` `instMembership` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid`	—	—	`antidiagonal_congr` `swap_mem_antidiagonal`
`antidiagonal_subtype_ext` 📖	—	`Finset` `SetLike.instMembership` `instSetLike` `HasAntidiagonal.antidiagonal` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid`	—	—	`antidiagonal_congr` `Subtype.prop`
`antidiagonal_subtype_ext_iff` 📖	mathematical	—	`Finset` `SetLike.instMembership` `instSetLike` `HasAntidiagonal.antidiagonal` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid`	—	`antidiagonal_subtype_ext`
`antidiagonal_zero` 📖	mathematical	—	`HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finset` `instSingleton`	—	`ext` `Unique.instSubsingleton`
`filter_fst_eq_antidiagonal` 📖	mathematical	—	`filter` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `instSingleton` `instEmptyCollection`	—	`ext` `le_add_right` `le_rfl` `add_tsub_cancel_left` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono` `mem_filter` `HasAntidiagonal.mem_antidiagonal` `mem_singleton` `ite_prop_iff_or`
`filter_snd_eq_antidiagonal` 📖	mathematical	—	`filter` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `instSingleton` `instEmptyCollection`	—	`Prod.swap_injective` `map_swap_antidiagonal` `filter_map` `filter.congr_simp` `filter_fst_eq_antidiagonal` `map_singleton`
`hasAntidiagonal_congr` 📖	mathematical	—	`HasAntidiagonal.antidiagonal`	—	`instSubsingletonHasAntidiagonal`
`instSubsingletonHasAntidiagonal` 📖	mathematical	—	`HasAntidiagonal`	—	`ext`
`map_prodComm_antidiagonal` 📖	mathematical	—	`map` `Equiv.toEmbedding` `Equiv.prodComm` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	—	`ext` `add_comm`
`map_swap_antidiagonal` 📖	mathematical	—	`map` `Prod.swap_injective` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	—	`map_prodComm_antidiagonal`
`sigmaAntidiagonalEquivProd_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `instSetLike` `HasAntidiagonal.antidiagonal` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaAntidiagonalEquivProd`	—	—
`sigmaAntidiagonalEquivProd_symm_apply_fst` 📖	mathematical	—	`Finset` `SetLike.instMembership` `instSetLike` `HasAntidiagonal.antidiagonal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sigmaAntidiagonalEquivProd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`sigmaAntidiagonalEquivProd_symm_apply_snd_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `instSetLike` `HasAntidiagonal.antidiagonal` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sigmaAntidiagonalEquivProd`	—	—
`swap_mem_antidiagonal` 📖	mathematical	—	`Finset` `instMembership` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	—	`add_comm`

Finset.HasAntidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_antidiagonal` 📖	mathematical	—	`Finset` `Finset.instMembership` `antidiagonal` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—

Finset.antidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_le` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder`	—	`le_iff_exists_add` `Finset.HasAntidiagonal.mem_antidiagonal`
`snd_le` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder`	—	`le_iff_exists_add` `add_comm` `Finset.HasAntidiagonal.mem_antidiagonal`

---

← Back to Index