MulAntidiagonal

📁 Source: Mathlib/Data/Set/MulAntidiagonal.lean

Statistics

Metric	Count
Definitions addAntidiagonal, mulAntidiagonal	2
Theorems eq_of_fst_eq_fst, eq_of_fst_le_fst_of_snd_le_snd, eq_of_snd_eq_snd, finite_of_isPWO, finite_of_isWF, fst_eq_fst_iff_snd_eq_snd, eq_of_fst_eq_fst, eq_of_fst_le_fst_of_snd_le_snd, eq_of_snd_eq_snd, finite_of_isPWO, finite_of_isWF, fst_eq_fst_iff_snd_eq_snd, addAntidiagonal_mono_left, addAntidiagonal_mono_right, mem_addAntidiagonal, mem_mulAntidiagonal, mulAntidiagonal_mono_left, mulAntidiagonal_mono_right, swap_mem_addAntidiagonal, swap_mem_addAntidiagonal_aux, swap_mem_mulAntidiagonal, swap_mem_mulAntidiagonal_aux	22
Total	24

Set

Definitions

Name	Category	Theorems
addAntidiagonal 📖	CompOp	8 math math: AddAntidiagonal.finite_of_isWF, addAntidiagonal_mono_left, swap_mem_addAntidiagonal_aux, mem_addAntidiagonal, swap_mem_addAntidiagonal, AddAntidiagonal.finite_of_isPWO, AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd, addAntidiagonal_mono_right
mulAntidiagonal 📖	CompOp	8 math math: mulAntidiagonal_mono_left, MulAntidiagonal.finite_of_isPWO, mulAntidiagonal_mono_right, MulAntidiagonal.finite_of_isWF, MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd, swap_mem_mulAntidiagonal_aux, swap_mem_mulAntidiagonal, mem_mulAntidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addAntidiagonal_mono_left 📖	mathematical	Set instHasSubset	addAntidiagonal	—	—
addAntidiagonal_mono_right 📖	mathematical	Set instHasSubset	addAntidiagonal	—	—
mem_addAntidiagonal 📖	mathematical	—	Set instMembership addAntidiagonal	—	—
mem_mulAntidiagonal 📖	mathematical	—	Set instMembership mulAntidiagonal	—	—
mulAntidiagonal_mono_left 📖	mathematical	Set instHasSubset	mulAntidiagonal	—	—
mulAntidiagonal_mono_right 📖	mathematical	Set instHasSubset	mulAntidiagonal	—	—
swap_mem_addAntidiagonal 📖	mathematical	—	Set instMembership addAntidiagonal AddCommMagma.toAdd	—	mem_addAntidiagonal add_comm
swap_mem_addAntidiagonal_aux 📖	mathematical	—	Set instMembership AddCommMagma.toAdd addAntidiagonal	—	add_comm mem_addAntidiagonal
swap_mem_mulAntidiagonal 📖	mathematical	—	Set instMembership mulAntidiagonal CommMagma.toMul	—	mul_comm
swap_mem_mulAntidiagonal_aux 📖	mathematical	—	Set instMembership CommMagma.toMul mulAntidiagonal	—	mul_comm

Set.AddAntidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_fst_eq_fst 📖	—	Set Set.instMembership Set.addAntidiagonal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	fst_eq_fst_iff_snd_eq_snd
eq_of_fst_le_fst_of_snd_le_snd 📖	—	Preorder.toLE PartialOrder.toPreorder Set Set.instMembership Set.addAntidiagonal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	eq_of_fst_eq_fst LE.le.eq_of_not_lt LT.lt.ne add_lt_add_of_lt_of_le Set.mem_addAntidiagonal
eq_of_snd_eq_snd 📖	—	Set Set.instMembership Set.addAntidiagonal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	fst_eq_fst_iff_snd_eq_snd
finite_of_isPWO 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set.Finite Set.addAntidiagonal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Set.mem_addAntidiagonal Set.not_finite Set.PartiallyWellOrderedOn.exists_monotone_subseq Order.Preimage.instIsPreorder instIsPreorderLe LT.lt.ne RelEmbedding.injective Function.Embedding.injective eq_of_fst_le_fst_of_snd_le_snd LT.lt.le
finite_of_isWF 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.Finite Set.addAntidiagonal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid	—	finite_of_isPWO AddCancelMonoid.toIsCancelAdd Set.IsWF.isPWO
fst_eq_fst_iff_snd_eq_snd 📖	mathematical	—	Set Set.instMembership Set.addAntidiagonal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	add_left_cancel IsCancelAdd.toIsLeftCancelAdd add_right_cancel IsCancelAdd.toIsRightCancelAdd

Set.MulAntidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_fst_eq_fst 📖	—	Set Set.instMembership Set.mulAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—	fst_eq_fst_iff_snd_eq_snd
eq_of_fst_le_fst_of_snd_le_snd 📖	—	Preorder.toLE PartialOrder.toPreorder Set Set.instMembership Set.mulAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—	eq_of_fst_eq_fst LE.le.eq_of_not_lt LT.lt.ne mul_lt_mul_of_lt_of_le Set.mem_mulAntidiagonal
eq_of_snd_eq_snd 📖	—	Set Set.instMembership Set.mulAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—	fst_eq_fst_iff_snd_eq_snd
finite_of_isPWO 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set.Finite Set.mulAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Set.mem_mulAntidiagonal Set.PartiallyWellOrderedOn.exists_monotone_subseq Order.Preimage.instIsPreorder instIsPreorderLe LT.lt.ne RelEmbedding.injective Function.Embedding.injective eq_of_fst_le_fst_of_snd_le_snd LT.lt.le
finite_of_isWF 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.Finite Set.mulAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid CancelCommMonoid.toCommMonoid	—	finite_of_isPWO CancelMonoid.toIsCancelMul Set.IsWF.isPWO
fst_eq_fst_iff_snd_eq_snd 📖	mathematical	—	Set Set.instMembership Set.mulAntidiagonal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	mul_left_cancel IsCancelMul.toIsLeftCancelMul mul_right_cancel IsCancelMul.toIsRightCancelMul

---

← Back to Index