MulAntidiagonal

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

Statistics

Metric	Count
Definitions addAntidiagonal, mulAntidiagonal	2
Theorems addAntidiagonal_min_add_min, addAntidiagonal_mono_left, addAntidiagonal_mono_right, isPWO_support_addAntidiagonal, isPWO_support_mulAntidiagonal, mem_addAntidiagonal, mem_mulAntidiagonal, mulAntidiagonal_min_mul_min, mulAntidiagonal_mono_left, mulAntidiagonal_mono_right, support_addAntidiagonal_subset_add, support_mulAntidiagonal_subset_mul, swap_mem_addAntidiagonal, swap_mem_mulAntidiagonal, add, mul, add, min_add, min_mul, mul	20
Total	22

Finset

Definitions

Name	Category	Theorems
addAntidiagonal 📖	CompOp	11 math math: HahnSeries.coeff_mul, HahnSeries.SummableFamily.coeff_hsum_mul, HahnSeries.coeff_mul_left', addAntidiagonal_mono_right, addAntidiagonal_min_add_min, swap_mem_addAntidiagonal, isPWO_support_addAntidiagonal, support_addAntidiagonal_subset_add, HahnSeries.coeff_mul_right', mem_addAntidiagonal, addAntidiagonal_mono_left
mulAntidiagonal 📖	CompOp	7 math math: swap_mem_mulAntidiagonal, mem_mulAntidiagonal, mulAntidiagonal_mono_left, mulAntidiagonal_mono_right, isPWO_support_mulAntidiagonal, mulAntidiagonal_min_mul_min, support_mulAntidiagonal_subset_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addAntidiagonal_min_add_min 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	addAntidiagonal Set.IsWF.isPWO AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.IsWF.min Finset instSingleton	—	ext Set.IsWF.isPWO mem_addAntidiagonal mem_singleton add_left_cancel IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd LE.le.eq_of_not_lt Set.IsWF.min_le LT.lt.ne' add_lt_add_of_lt_of_le IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd covariant_swap_add_of_covariant_add Set.IsWF.min_mem
addAntidiagonal_mono_left 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset addAntidiagonal	—	Set.Finite.toFinset_mono Set.addAntidiagonal_mono_left
addAntidiagonal_mono_right 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset addAntidiagonal	—	Set.Finite.toFinset_mono Set.addAntidiagonal_mono_right
isPWO_support_addAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	setOf Nonempty addAntidiagonal	—	Set.IsPWO.mono Set.IsPWO.add support_addAntidiagonal_subset_add
isPWO_support_mulAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	setOf Nonempty mulAntidiagonal	—	Set.IsPWO.mono Set.IsPWO.mul support_mulAntidiagonal_subset_mul
mem_addAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Finset instMembership addAntidiagonal Set Set.instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Set.Finite.mem_toFinset Set.mem_addAntidiagonal
mem_mulAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Finset instMembership mulAntidiagonal Set Set.instMembership MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—
mulAntidiagonal_min_mul_min 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	mulAntidiagonal Set.IsWF.isPWO MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Set.IsWF.min Finset instSingleton	—	ext Set.IsWF.isPWO mul_left_cancel IsCancelMul.toIsLeftCancelMul IsOrderedCancelMonoid.toIsCancelMul LE.le.eq_of_not_lt Set.IsWF.min_le LT.lt.ne' mul_lt_mul_of_lt_of_le IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid IsRightCancelMul.mulRightStrictMono_of_mulRightMono IsCancelMul.toIsRightCancelMul covariant_swap_mul_of_covariant_mul Set.IsWF.min_mem
mulAntidiagonal_mono_left 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset mulAntidiagonal	—	Set.Finite.toFinset_mono Set.mulAntidiagonal_mono_left
mulAntidiagonal_mono_right 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set Set.instHasSubset	Finset instHasSubset mulAntidiagonal	—	Set.Finite.toFinset_mono Set.mulAntidiagonal_mono_right
support_addAntidiagonal_subset_add 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set Set.instHasSubset setOf Nonempty addAntidiagonal Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	mem_addAntidiagonal
support_mulAntidiagonal_subset_mul 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set Set.instHasSubset setOf Nonempty mulAntidiagonal Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	mem_mulAntidiagonal
swap_mem_addAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Finset instMembership addAntidiagonal	—	mem_addAntidiagonal Set.swap_mem_addAntidiagonal_aux Set.mem_addAntidiagonal
swap_mem_mulAntidiagonal 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Finset instMembership mulAntidiagonal	—	—

Set.IsPWO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Set.add_image_prod image_of_monotone prod Monotone.add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add monotone_fst monotone_snd
mul 📖	mathematical	Set.IsPWO PartialOrder.toPreorder	Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Set.image_mul_prod image_of_monotone prod Monotone.mul' IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid covariant_swap_mul_of_covariant_mul monotone_fst monotone_snd

Set.IsWF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Set.IsPWO.isWF Set.IsPWO.add isPWO
min_add 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	min Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid add Set.Nonempty.add	—	le_antisymm add Set.Nonempty.add min_le Set.mem_add min_mem le_min_iff add_le_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add
min_mul 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	min Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid mul Set.Nonempty.mul	—	le_antisymm mul Set.Nonempty.mul min_le Set.mem_mul min_mem le_min_iff mul_le_mul' IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid covariant_swap_mul_of_covariant_mul
mul 📖	mathematical	Set.IsWF Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Set.IsPWO.isWF Set.IsPWO.mul isPWO

---

← Back to Index