Permanent

📁 Source: Mathlib/LinearAlgebra/Matrix/Permanent.lean

Statistics

Metric	Count
Definitions permanent	1
Theorems permanent_diagonal, permanent_eq_elem_of_card_eq_one, permanent_eq_elem_of_subsingleton, permanent_eq_one_of_card_eq_zero, permanent_isEmpty, permanent_one, permanent_permute_cols, permanent_permute_rows, permanent_smul, permanent_transpose, permanent_unique, permanent_updateCol_smul, permanent_updateRow_smul, permanent_zero	14
Total	15

Matrix

Definitions

Name	Category	Theorems
permanent 📖	CompOp	14 math math: permanent_unique, permanent_eq_elem_of_card_eq_one, permanent_permute_rows, permanent_eq_elem_of_subsingleton, permanent_updateRow_smul, permanent_one, permanent_updateCol_smul, permanent_permute_cols, permanent_diagonal, permanent_zero, permanent_eq_one_of_card_eq_zero, permanent_transpose, permanent_smul, permanent_isEmpty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
permanent_diagonal 📖	mathematical	—	permanent diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.prod CommSemiring.toCommMonoid Finset.univ	—	Finset.sum_eq_single Equiv.ext Finset.prod_eq_zero Finset.mem_univ Finset.prod_congr diagonal_apply_eq
permanent_eq_elem_of_card_eq_one 📖	mathematical	Fintype.card	permanent	—	permanent_eq_elem_of_subsingleton Fintype.card_le_one_iff_subsingleton Eq.le
permanent_eq_elem_of_subsingleton 📖	mathematical	—	permanent	—	Lean.Meta.FastSubsingleton.elim permanent_unique
permanent_eq_one_of_card_eq_zero 📖	mathematical	Fintype.card	permanent AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	permanent_isEmpty Fintype.card_eq_zero_iff
permanent_isEmpty 📖	mathematical	—	permanent AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Finset.sum_congr Finset.univ_unique IsEmpty.instSubsingleton Finset.prod_congr Finset.univ_eq_empty Finset.sum_const Finset.card_singleton one_smul
permanent_one 📖	mathematical	—	permanent Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	diagonal_one permanent_diagonal Finset.prod_const_one
permanent_permute_cols 📖	mathematical	—	permanent submatrix DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	Function.Bijective.sum_comp Group.mulLeft_bijective
permanent_permute_rows 📖	mathematical	—	permanent submatrix DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	permanent_transpose transpose_submatrix permanent_permute_cols
permanent_smul 📖	mathematical	—	permanent Matrix smul Algebra.toSMul CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Fintype.card	—	Finset.sum_congr Finset.prod_congr Finset.mul_sum mul_comm Finset.prod_mul_pow_card
permanent_transpose 📖	mathematical	—	permanent transpose	—	Fintype.sum_bijective Function.Involutive.bijective inv_involutive Fintype.prod_equiv Equiv.symm_apply_apply
permanent_unique 📖	mathematical	—	permanent Unique.instInhabited	—	Finset.sum_congr Finset.univ_unique Unique.instSubsingleton Finset.prod_congr Finset.prod_singleton Finset.sum_singleton
permanent_updateCol_smul 📖	mathematical	—	permanent updateCol Function.hasSMul Algebra.toSMul CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Finset.sum_congr Finset.mul_prod_erase Finset.mem_univ updateCol_self Finset.mul_sum Finset.prod_congr updateCol_ne Finset.ne_of_mem_erase
permanent_updateRow_smul 📖	mathematical	—	permanent updateRow Function.hasSMul Algebra.toSMul CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	permanent_transpose updateCol_transpose permanent_updateCol_smul
permanent_zero 📖	mathematical	—	permanent Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Finset.sum_congr Finset.prod_congr Finset.prod_const zero_pow Finset.sum_const_zero

---

← Back to Index