Sum

📁 Source: Mathlib/Data/Fintype/Sum.lean

Statistics

Metric	Count
Definitions fintypeOfFintypeNe, instFintypeSum	2
Theorems exists_equiv_extend_of_card_eq, toLeft_eq_empty, toLeft_eq_univ, toLeft_univ, toRight_eq_empty, toRight_eq_univ, toRight_univ, univ_disjSum_univ, card_subtype_eq_or_eq_of_ne, card_subtype_or, card_subtype_or_disjoint, card_sum, exists_equiv_extend_of_card_eq, image_subtype_ne_univ_eq_image_erase, image_subtype_univ_ssubset_image_univ, infinite_sum	16
Total	18

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_equiv_extend_of_card_eq 📖	mathematical	Fintype.card card Finset instHasSubset image Set.InjOn SetLike.coe instSetLike	SetLike.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	induction Fintype.card_eq Fintype.card_coe instIsEmptyFalse LE.le.trans image_mono subset_insert Set.InjOn.mono mem_image_of_mem mem_insert_self Equiv.swap_apply_right Equiv.trans_apply Equiv.swap_apply_of_ne_of_ne ne_of_eq_of_ne Set.InjOn.ne Equiv.injective
toLeft_eq_empty 📖	mathematical	—	toLeft Finset instEmptyCollection instHasSubset map Function.Embedding.inr univ	—	—
toLeft_eq_univ 📖	mathematical	—	toLeft univ Finset instHasSubset map Function.Embedding.inl	—	—
toLeft_univ 📖	mathematical	—	toLeft univ instFintypeSum	—	ext
toRight_eq_empty 📖	mathematical	—	toRight Finset instEmptyCollection instHasSubset map Function.Embedding.inl univ	—	—
toRight_eq_univ 📖	mathematical	—	toRight univ Finset instHasSubset map Function.Embedding.inr	—	—
toRight_univ 📖	mathematical	—	toRight univ instFintypeSum	—	ext
univ_disjSum_univ 📖	mathematical	—	disjSum univ instFintypeSum	—	—

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_subtype_eq_or_eq_of_ne 📖	mathematical	—	card Subtype.fintype	—	card_subtype_or_disjoint
card_subtype_or 📖	mathematical	—	card	—	card_sum card_le_of_embedding
card_subtype_or_disjoint 📖	mathematical	Disjoint Pi.partialOrder Prop.partialOrder Pi.instOrderBot Prop.le HeytingAlgebra.toOrderBot Prop.instHeytingAlgebra	card	—	card_sum card_congr
card_sum 📖	mathematical	—	card instFintypeSum	—	Finset.card_disjSum

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_equiv_extend_of_card_eq 📖	mathematical	Fintype.card Finset.card Set.MapsTo SetLike.coe Finset Finset.instSetLike Set.InjOn	SetLike.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Finset.coe_image Set.coe_toFinset Finset.exists_equiv_extend_of_card_eq

(root)

Definitions

Name	Category	Theorems
fintypeOfFintypeNe 📖	CompOp	—
instFintypeSum 📖	CompOp	145 math math: SymplecticGroup.transpose_mem_iff, AlternatingMap.domCoprod.summand_mk'', Matrix.invOf_fromBlocks₂₂_eq, RootPairing.GeckConstruction.isSl2Triple, Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col, IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph, RootPairing.GeckConstruction.instHasTrivialRadical, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, SymplecticGroup.coe_inv, Finset.univ_disjSum_univ, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, SymplecticGroup.coe_J, Matrix.Pivot.listTransvecCol_mul_last_col, Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff, RootPairing.GeckConstruction.trace_h_eq_zero, AlternatingMap.domCoprod_coe, Matrix.fromBlocks_eq_of_invertible₁₁, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, LieAlgebra.Orthogonal.jb_transform, SymplecticGroup.mem_iff, Matrix.Pivot.mul_listTransvecRow_last_col, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, OrthonormalBasis.prod_apply, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, Module.Basis.prod_addHaar, Matrix.vecMul_fromRows, RootPairing.GeckConstruction.lie_h_e, Fintype.sum_sum_type, Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, Matrix.isUnit_fromBlocks_zero₂₁, Matrix.fromBlocks_mul_fromRows, Finset.toLeft_univ, Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm, Matrix.charpoly_fromBlocks_zero₂₁, Matrix.J_squared, Equiv.Perm.sign_sumCongr, RootPairing.GeckConstruction.trace_toEnd_eq_zero, Matrix.charmatrix_fromBlocks, Matrix.vecMul_fromBlocks, MultilinearMap.domCoprod_alternization_eq, Matrix.isUnit_det_J, Matrix.schur_complement_eq₂₂, RootPairing.GeckConstruction.span_range_h'_eq_top, Matrix.fromBlocks_mulVec, Finset.toRight_univ, addRothNumber_le_ruzsaSzemerediNumber, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', Matrix.TransvectionStruct.mul_sumInl_toMatrix_prod, Matrix.det_fromBlocks₁₁, sumElim_dotProduct_sumElim, Matrix.det_fromBlocks_one₁₁, RootPairing.GeckConstruction.ω_mul_h, Matrix.invOf_fromBlocks_zero₁₂_eq, RootPairing.GeckConstruction.instIsIrreducible, SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image, Module.Basis.prod_parallelepiped, IsometryEquiv.sumArrowIsometryEquivProdArrow_symm_apply, Matrix.isUnit_fromBlocks_iff_of_invertible₂₂, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, Matrix.det_toBlock, NumberField.mixedEmbedding.det_matrixToStdBasis, Matrix.fromBlocks_eq_of_invertible₂₂, Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction, Matrix.schur_complement_eq₁₁, Matrix.Pivot.mul_listTransvecRow_last_row, Matrix.det_fromBlocks_one₂₂, Matrix.isUnit_fromBlocks_zero₁₂, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, SymplecticGroup.mem_iff', Matrix.isUnit_fromBlocks_iff_of_invertible₁₁, LinearMap.toMatrix_prodMap, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, RootPairing.GeckConstruction.ωConj_invFun, Matrix.Pivot.listTransvecCol_mul_last_row_drop, Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row, Matrix.dotProduct_block, RootPairing.GeckConstruction.isNilpotent_f, RootPairing.GeckConstruction.lie_e_f_same, RootPairing.GeckConstruction.ω_mul_ω, RootPairing.GeckConstruction.f_lie_v_ne, RootPairing.GeckConstruction.ωConj_toFun, Matrix.charpoly_fromBlocks_zero₁₂, RootPairing.GeckConstruction.e_lie_v_ne, Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, RootPairing.GeckConstruction.ω_mul_e, RootPairing.GeckConstruction.isNilpotent_e, Matrix.det_fromBlocks₂₂, MultilinearMap.domCoprod_alternization, LieAlgebra.Orthogonal.jd_transform, Matrix.fromCols_mul_fromRows_eq_one_comm, Matrix.Pivot.mul_listTransvecRow_last_col_take, RootPairing.GeckConstruction.h_mem_lieAlgebra, Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero, Matrix.det_fromBlocks_zero₁₂, Matrix.Pivot.listTransvecCol_mul_last_row, Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff, SimpleGraph.TripartiteFromTriangles.card_triangles, RootPairing.GeckConstruction.lie_h_f, Matrix.J_inv, RootPairing.GeckConstruction.ω_mul_f, Polynomial.toMatrix_sylvesterMap, RootPairing.GeckConstruction.lie_e_lie_f_apply, Matrix.det_fromBlocks_zero₂₁, Matrix.invOf_fromBlocks_zero₂₁_eq, Matrix.sumElim_vecMul_fromRows, RootPairing.GeckConstruction.f_lie_v_same, Matrix.J_det_mul_J_det, Matrix.TransvectionStruct.sumInl_toMatrix_prod_mul, SymplecticGroup.coe_inv', Fintype.prod_sumElim, LieAlgebra.Orthogonal.pso_inv, MeasureTheory.measurePreserving_sumPiEquivProdPi_symm, Matrix.fromBlocks_multiply, Matrix.fromCols_mulVec_sumElim, RootPairing.GeckConstruction.f_mem_lieAlgebra, LieAlgebra.Orthogonal.indefiniteDiagonal_transform, RootPairing.GeckConstruction.e_mem_lieAlgebra, LieAlgebra.Orthogonal.pb_inv, RootPairing.GeckConstruction.lie_h_h, Fintype.prod_sum_type, Matrix.fromCols_mul_fromRows, AlternatingMap.domCoprod_apply, Fintype.sum_sumElim, MeasureTheory.volume_measurePreserving_sumPiEquivProdPi, Matrix.fromCols_mulVec, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, IsometryEquiv.sumArrowIsometryEquivProdArrow_apply, Matrix.fromCols_mul_fromBlocks, MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm, SimpleGraph.TripartiteFromTriangles.farFromTriangleFree, Matrix.invOf_fromBlocks₁₁_eq, RootPairing.GeckConstruction.lie_e_f_mul_ω, SymplecticGroup.J_mem, Fintype.card_sum, MeasureTheory.measurePreserving_sumPiEquivProdPi, PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp, RootPairing.GeckConstruction.e_lie_u, RootPairing.GeckConstruction.lie_e_f_ne, Matrix.fromBlocks_diagonal_pow, LieAlgebra.Orthogonal.pd_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_subtype_ne_univ_eq_image_erase 📖	mathematical	—	Finset.image Finset.univ Subtype.fintype Finset.erase	—	subset_antisymm Finset.instAntisymmSubset Finset.image_subset_iff Finset.mem_erase_of_ne_of_mem Finset.mem_image_of_mem Finset.mem_univ Finset.mem_image Finset.erase_subset Finset.ne_of_mem_erase
image_subtype_univ_ssubset_image_univ 📖	mathematical	Finset Finset.instMembership Finset.image Finset.univ	Finset.instHasSSubset Subtype.fintype	—	—
infinite_sum 📖	mathematical	—	Infinite	—	Mathlib.Tactic.Contrapose.contrapose₁ Finite.of_fintype Sum.infinite_of_left Sum.infinite_of_right

---

← Back to Index