Basis

📁 Source: Mathlib/Data/Matrix/Basis.lean

Statistics

Metric	Count
Definitions liftLinear, single, singleAddMonoidHom, singleLinearMap	4
Theorems center_eq_range, center_eq_scalar_image, col_eq_zero_of_commute_single, diag_eq_of_commute_single, diag_single_of_ne, diag_single_same, diagonal_single, ext_addMonoidHom, ext_addMonoidHom_iff, ext_linearMap, ext_linearMap_iff, induction_on, induction_on', liftLinear_apply, liftLinear_comp_singleLinearMap, liftLinear_single, liftLinear_singleLinearMap, map_single, matrix_eq_sum_single, mem_range_scalar_iff_commute_single, mem_range_scalar_iff_commute_single', mem_range_scalar_of_commute_single, mul_single_apply_of_ne, mul_single_apply_same, of_symm_single, row_eq_zero_of_commute_single, singleAddMonoidHom_apply, singleLinearMap_apply, single_add, single_apply, single_apply_of_col_ne, single_apply_of_ne, single_apply_of_row_ne, single_apply_same, single_eq_of_single_single, single_eq_single_vecMulVec_single, single_mem_matrix, single_mulVec, single_mul_apply_of_ne, single_mul_apply_same, single_mul_mul_single, single_mul_single_of_ne, single_mul_single_same, single_zero, smul_single, submatrix_single_equiv, submonoidCenter_eq_scalar_map, subringCenter_eq_scalar_map, subsemigroupCenter_eq_scalar_map, subsemiringCenter_eq_scalar_map, sum_single_eq_diagonal, sum_single_intCast, sum_single_natCast, sum_single_ofNat, sum_single_one, sum_sum_single, transpose_single	57
Total	61

Matrix

Definitions

Name	Category	Theorems
liftLinear 📖	CompOp	4 math math: liftLinear_single, liftLinear_singleLinearMap, liftLinear_comp_singleLinearMap, liftLinear_apply
single 📖	CompOp	75 math math: single_eq_updateRow_zero, single_hadamard_single_eq, kroneckerTMulAlgEquiv_symm_single_tmul, mul_single_apply_same, liftLinear_single, trace_single_eq_same, single_add, sum_single_one, single_apply_of_ne, matrix_eq_sum_single, sum_sum_single, comp_single_single, single_zero, submatrix_single_equiv, single_eq_single_vecMulVec_single, matPolyEquiv_coeff_apply_aux_1, Module.Basis.matrix_apply, single_mem_matrix, RingCon.ofMatrix_rel, Ideal.single_mem_jacobson_matrix, singleLinearMap_apply, vec_single, singleAddMonoidHom_apply, mul_single_apply_of_ne, single_mul_apply_same, mem_range_scalar_iff_commute_single, single_kroneckerTMul_single, single_kronecker_single, sum_single_ofNat, mul_single_eq_updateCol_zero, toMatrix_dualTensorHom, MatrixModCat.mem_toModuleCatObj, single_apply_of_row_ne, RingCon.ofMatrix_rel', single_mul_single_same, blockTriangular_single, map_single, trace_single_eq_of_ne, single_hadamard_single_of_ne, mem_range_scalar_iff_commute_single', single_mul_mul_single, matrixEquivTensor_apply_single, trace_single_mul, kroneckerMap_single_single, single_mul_single_of_ne, single_mul_eq_updateRow_zero, RingCon.matrix_apply_single, stdBasis_eq_single, transpose_single, LieAlgebra.SpecialLinear.val_single, Module.single_smul, diag_single_same, trace_mul_single, of_symm_single, single_apply_same, single_eq_of_single_single, sum_single_intCast, updateRow_zero_mul_updateCol_zero, sum_single_natCast, conjTranspose_single, single_eq_updateCol_zero, sum_single_eq_diagonal, single_mulVec, smul_single, diagonal_single, single_apply, single_mul_apply_of_ne, LieAlgebra.SpecialLinear.val_singleSubSingle, matPolyEquiv_coeff_apply_aux_2, matrixEquivTensor_apply, comp_symm_single, single_apply_of_col_ne, blockTriangular_single', diag_single_of_ne, gram_single
singleAddMonoidHom 📖	CompOp	2 math math: singleAddMonoidHom_apply, ext_addMonoidHom_iff
singleLinearMap 📖	CompOp	4 math math: liftLinear_singleLinearMap, liftLinear_comp_singleLinearMap, singleLinearMap_apply, ext_linearMap_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_range 📖	mathematical	—	Set.center Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Set.range DFunLike.coe RingHom nonAssocSemiring RingHom.instFunLike scalar	—	center_eq_scalar_image Set.center_eq_univ Set.image_univ
center_eq_scalar_image 📖	mathematical	—	Set.center Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Set.image DFunLike.coe RingHom nonAssocSemiring RingHom.instFunLike scalar	—	Set.ext isEmpty_or_nonempty MulZeroClass.mul_zero MulZeroClass.zero_mul diagonal_zero subsingleton_of_empty_right mem_range_scalar_iff_commute_single' mul_diagonal single_apply_same mul_single_apply_same diagonal_apply_eq Commute.symm scalar_commute
col_eq_zero_of_commute_single 📖	—	Commute Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	ext_iff single_mul_apply_of_ne mul_single_apply_same mul_one
diag_eq_of_commute_single 📖	—	Commute Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	ext_iff single_mul_apply_same one_mul mul_single_apply_same mul_one
diag_single_of_ne 📖	mathematical	—	diag single Pi.instZero	—	—
diag_single_same 📖	mathematical	—	diag single Pi.single	—	single_apply_same Pi.single_eq_same single_apply_of_ne Pi.single_eq_of_ne'
diagonal_single 📖	mathematical	—	diagonal Pi.single single	—	ext
ext_addMonoidHom 📖	—	AddMonoidHom.comp Matrix AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addZeroClass singleAddMonoidHom	—	—	nonempty_fintype AddMonoidHom.ext matrix_eq_sum_single map_sum AddMonoidHom.instAddMonoidHomClass Finset.sum_congr DFunLike.congr_fun
ext_addMonoidHom_iff 📖	mathematical	—	AddMonoidHom.comp Matrix AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addZeroClass singleAddMonoidHom	—	ext_addMonoidHom
ext_linearMap 📖	—	LinearMap.comp Matrix addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids singleLinearMap	—	—	RingHomCompTriple.ids LinearMap.toAddMonoidHom_injective ext_addMonoidHom
ext_linearMap_iff 📖	mathematical	—	LinearMap.comp Matrix addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids singleLinearMap	—	RingHomCompTriple.ids ext_linearMap
induction_on 📖	—	Matrix add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	induction_on' single_zero
induction_on' 📖	—	Matrix zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup single	—	—	nonempty_fintype matrix_eq_sum_single Finset.sum_product' Finset.sum_induction
liftLinear_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix addCommMonoid module LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike liftLinear Finset.sum Finset.univ	—	RingHomInvPair.ids RingHomCompTriple.ids Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.coe_sum Finset.sum_apply
liftLinear_comp_singleLinearMap 📖	mathematical	—	LinearMap.comp Matrix addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike liftLinear singleLinearMap	—	LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids liftLinear_single
liftLinear_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix addCommMonoid module LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike liftLinear single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids of_symm_single LinearMap.lsum_piSingle
liftLinear_singleLinearMap 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid module Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike liftLinear singleLinearMap LinearMap.id	—	ext_linearMap Finite.of_fintype RingHomInvPair.ids smulCommClass liftLinear_comp_singleLinearMap
map_single 📖	mathematical	—	map single DFunLike.coe	—	ext map_zero
matrix_eq_sum_single 📖	mathematical	—	Finset.sum Matrix addCommMonoid Finset.univ single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_sum_single
mem_range_scalar_iff_commute_single 📖	mathematical	—	Matrix Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring nonAssocSemiring RingHom.instFunLike scalar Commute instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Commute.symm scalar_commute_iff smul_single mul_one one_mul mem_range_scalar_of_commute_single
mem_range_scalar_iff_commute_single' 📖	mathematical	—	Matrix Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring nonAssocSemiring RingHom.instFunLike scalar Commute instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Commute.symm scalar_commute_iff smul_single mul_one one_mul mem_range_scalar_iff_commute_single
mem_range_scalar_of_commute_single 📖	mathematical	Pairwise Commute Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Set Set.instMembership Set.range DFunLike.coe RingHom nonAssocSemiring RingHom.instFunLike scalar	—	isEmpty_or_nonempty subsingleton_of_empty_right ext Decidable.eq_or_ne diagonal_apply_eq diag_eq_of_commute_single diagonal_apply_ne col_eq_zero_of_commute_single row_eq_zero_of_commute_single
mul_single_apply_of_ne 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr single_apply_of_ne MulZeroClass.mul_zero Finset.sum_const_zero
mul_single_apply_same 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr mul_ite MulZeroClass.mul_zero Finset.sum_ite_eq
of_symm_single 📖	mathematical	—	DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Equiv.symm of single Pi.single Pi.instZero	—	single_eq_of_single_single
row_eq_zero_of_commute_single 📖	—	Commute Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	ext_iff single_mul_apply_same one_mul mul_single_apply_of_ne
singleAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Matrix AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addZeroClass AddMonoidHom.instFunLike singleAddMonoidHom single AddZero.toZero	—	—
singleLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix addCommMonoid module LinearMap.instFunLike singleLinearMap single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
single_add 📖	mathematical	—	single AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd Matrix add	—	ext add_zero
single_apply 📖	mathematical	—	single	—	—
single_apply_of_col_ne 📖	mathematical	—	single	—	single_apply_of_ne
single_apply_of_ne 📖	mathematical	—	single	—	—
single_apply_of_row_ne 📖	mathematical	—	single	—	single_apply_of_ne
single_apply_same 📖	mathematical	—	single	—	—
single_eq_of_single_single 📖	mathematical	—	single DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike of Pi.single Pi.instZero	—	ext Pi.single_eq_same Pi.single_eq_of_ne'
single_eq_single_vecMulVec_single 📖	mathematical	—	single MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass vecMulVec MulZeroClass.toMul Pi.single	—	ite_and Pi.single_apply ite_mul one_mul MulZeroClass.zero_mul
single_mem_matrix 📖	mathematical	Set Set.instMembership	Matrix Set.matrix single	—	ite_mem
single_mulVec 📖	mathematical	—	mulVec single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Function.update Pi.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Finset.sum_congr ite_mul MulZeroClass.zero_mul eq_or_ne Finset.sum_ite_eq Function.update_self Finset.sum_const_zero Function.update_of_ne
single_mul_apply_of_ne 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr single_apply_of_ne MulZeroClass.zero_mul Finset.sum_const_zero
single_mul_apply_same 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr ite_mul MulZeroClass.zero_mul Finset.sum_ite_eq
single_mul_mul_single 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ext Finset.sum_congr ite_mul MulZeroClass.zero_mul Finset.sum_ite_eq mul_ite MulZeroClass.mul_zero Finset.sum_const_zero
single_mul_single_of_ne 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass zero	—	ext Finset.sum_congr mul_ite ite_mul MulZeroClass.zero_mul MulZeroClass.mul_zero Finset.sum_eq_zero instIsEmptyFalse Finset.sum_const_zero
single_mul_single_same 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ext Finset.sum_congr mul_ite ite_mul MulZeroClass.zero_mul MulZeroClass.mul_zero Finset.sum_ite_eq Finset.sum_const_zero
single_zero 📖	mathematical	—	single Matrix zero	—	ext
smul_single 📖	mathematical	—	Matrix smul SMulZeroClass.toSMul single	—	ext smul_ite smul_zero
submatrix_single_equiv 📖	mathematical	—	submatrix single DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	ext ne_or_eq single_apply_of_row_ne Iff.not Equiv.symm_apply_eq single_apply_of_col_ne single.congr_simp Equiv.apply_symm_apply single_apply_same
submonoidCenter_eq_scalar_map 📖	mathematical	—	Submonoid.center Matrix MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring Submonoid.map RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass scalar	—	SetLike.coe_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass center_eq_scalar_image
subringCenter_eq_scalar_map 📖	mathematical	—	Subring.center Matrix instRing Subring.map scalar Ring.toSemiring	—	SetLike.coe_injective center_eq_scalar_image
subsemigroupCenter_eq_scalar_map 📖	mathematical	—	Subsemigroup.center Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Subsemigroup.map MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring MonoidHom.toMulHom RingHom.toMonoidHom scalar	—	SetLike.coe_injective center_eq_scalar_image
subsemiringCenter_eq_scalar_map 📖	mathematical	—	Subsemiring.center Matrix nonAssocSemiring Semiring.toNonAssocSemiring Subsemiring.map scalar	—	SetLike.coe_injective center_eq_scalar_image
sum_single_eq_diagonal 📖	mathematical	—	Finset.sum Matrix addCommMonoid Finset.univ single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid diagonal	—	ext sum_apply diagonal_apply Finset.sum_eq_single instIsEmptyFalse
sum_single_intCast 📖	mathematical	—	Finset.sum Matrix addCommMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne Finset.univ single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroupWithOne.toAddCommGroup AddGroupWithOne.toIntCast AddCommGroupWithOne.toAddGroupWithOne instIntCastOfZero	—	sum_single_eq_diagonal
sum_single_natCast 📖	mathematical	—	Finset.sum Matrix addCommMonoid AddCommMonoidWithOne.toAddCommMonoid Finset.univ single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne AddMonoidWithOne.toNatCast instNatCastOfZero	—	sum_single_eq_diagonal
sum_single_ofNat 📖	mathematical	—	Finset.sum Matrix addCommMonoid AddCommMonoidWithOne.toAddCommMonoid Finset.univ single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne	—	sum_single_eq_diagonal
sum_single_one 📖	mathematical	—	Finset.sum Matrix addCommMonoid Finset.univ single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid one	—	sum_single_eq_diagonal
sum_sum_single 📖	mathematical	—	Finset.sum Matrix addCommMonoid Finset.univ single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike of	—	ext Fintype.sum_prod_type' Finset.sum_congr sum_apply Finset.sum_ite_eq'
transpose_single 📖	mathematical	—	transpose single	—	ext

---

← Back to Index