Normed

📁 Source: Mathlib/Analysis/Matrix/Normed.lean

Statistics

Metric	Count
Definitions frobeniusNormedAddCommGroup, frobeniusNormedAlgebra, frobeniusNormedRing, frobeniusNormedSpace, frobeniusSeminormedAddCommGroup, linftyOpNonUnitalNormedRing, linftyOpNonUnitalSemiNormedRing, linftyOpNormedAddCommGroup, linftyOpNormedAlgebra, linftyOpNormedRing, linftyOpNormedSpace, linftyOpSemiNormedRing, linftyOpSeminormedAddCommGroup, normedAddCommGroup, normedSpace, seminormedAddCommGroup	16
Theorems frobeniusIsBoundedSMul, frobeniusNormSMulClass, frobenius_nnnorm_conjTranspose, frobenius_nnnorm_def, frobenius_nnnorm_diagonal, frobenius_nnnorm_map_eq, frobenius_nnnorm_mul, frobenius_nnnorm_one, frobenius_nnnorm_replicateCol, frobenius_nnnorm_replicateRow, frobenius_nnnorm_transpose, frobenius_norm_conjTranspose, frobenius_norm_def, frobenius_norm_diagonal, frobenius_norm_map_eq, frobenius_norm_mul, frobenius_norm_replicateCol, frobenius_norm_replicateRow, frobenius_norm_transpose, frobenius_normedStarGroup, instNormOneClassOfNonempty, instNormedStarGroup, isBoundedSMul, linftyOpIsBoundedSMul, linftyOpNormSMulClass, linfty_opNNNorm_def, linfty_opNNNorm_diagonal, linfty_opNNNorm_eq_opNNNorm, linfty_opNNNorm_mul, linfty_opNNNorm_mulVec, linfty_opNNNorm_replicateCol, linfty_opNNNorm_replicateRow, linfty_opNNNorm_toMatrix, linfty_opNormOneClass, linfty_opNorm_def, linfty_opNorm_diagonal, linfty_opNorm_eq_opNorm, linfty_opNorm_mul, linfty_opNorm_mulVec, linfty_opNorm_replicateCol, linfty_opNorm_replicateRow, linfty_opNorm_toMatrix, nnnorm_conjTranspose, nnnorm_def, nnnorm_diagonal, nnnorm_entry_le_entrywise_sup_nnnorm, nnnorm_le_iff, nnnorm_lt_iff, nnnorm_map_eq, nnnorm_replicateCol, nnnorm_replicateRow, nnnorm_transpose, normSMulClass, norm_conjTranspose, norm_def, norm_diagonal, norm_entry_le_entrywise_sup_norm, norm_eq_sup_sup_nnnorm, norm_le_iff, norm_lt_iff, norm_map_eq, norm_replicateCol, norm_replicateRow, norm_transpose	64
Total	80

Matrix

Definitions

Name	Category	Theorems
frobeniusNormedAddCommGroup 📖	CompOp	1 math math: frobenius_norm_mul
frobeniusNormedAlgebra 📖	CompOp	—
frobeniusNormedRing 📖	CompOp	—
frobeniusNormedSpace 📖	CompOp	—
frobeniusSeminormedAddCommGroup 📖	CompOp	19 math math: frobenius_norm_replicateCol, frobenius_nnnorm_mul, frobeniusIsBoundedSMul, frobenius_nnnorm_map_eq, frobenius_normedStarGroup, frobenius_nnnorm_one, frobenius_norm_map_eq, frobenius_norm_conjTranspose, frobenius_norm_def, frobenius_nnnorm_replicateRow, frobenius_nnnorm_replicateCol, frobenius_nnnorm_diagonal, frobeniusNormSMulClass, frobenius_norm_diagonal, frobenius_nnnorm_def, frobenius_nnnorm_transpose, frobenius_norm_replicateRow, frobenius_nnnorm_conjTranspose, frobenius_norm_transpose
linftyOpNonUnitalNormedRing 📖	CompOp	—
linftyOpNonUnitalSemiNormedRing 📖	CompOp	1 math math: linfty_opNormOneClass
linftyOpNormedAddCommGroup 📖	CompOp	2 math math: linfty_opNorm_toMatrix, linfty_opNorm_eq_opNorm
linftyOpNormedAlgebra 📖	CompOp	—
linftyOpNormedRing 📖	CompOp	—
linftyOpNormedSpace 📖	CompOp	—
linftyOpSemiNormedRing 📖	CompOp	—
linftyOpSeminormedAddCommGroup 📖	CompOp	16 math math: linfty_opNorm_diagonal, linfty_opNorm_replicateRow, linfty_opNNNorm_mulVec, linfty_opNNNorm_eq_opNNNorm, linftyOpIsBoundedSMul, linfty_opNNNorm_toMatrix, linftyOpNormSMulClass, linfty_opNorm_mulVec, linfty_opNorm_replicateCol, linfty_opNNNorm_mul, linfty_opNorm_mul, linfty_opNNNorm_replicateCol, linfty_opNNNorm_replicateRow, linfty_opNNNorm_diagonal, linfty_opNNNorm_def, linfty_opNorm_def
normedAddCommGroup 📖	CompOp	1 math math: entrywise_sup_norm_bound_of_unitary
normedSpace 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	28 math math: norm_diagonal, norm_def, nnnorm_lt_iff, norm_entry_le_entrywise_sup_norm, isBoundedSMul, norm_map_eq, norm_le_iff, nnnorm_replicateRow, instNormOneClassOfNonempty, nnnorm_entry_le_entrywise_sup_nnnorm, norm_transpose, norm_replicateRow, nnnorm_transpose, Int.Matrix.one_le_norm_A_of_ne_zero, norm_conjTranspose, norm_lt_iff, nnnorm_conjTranspose, normSMulClass, nnnorm_diagonal, nnnorm_def, nnnorm_le_iff, norm_replicateCol, nnnorm_map_eq, instNormedStarGroup, Int.Matrix.exists_ne_zero_int_vec_norm_le, norm_eq_sup_sup_nnnorm, nnnorm_replicateCol, Int.Matrix.exists_ne_zero_int_vec_norm_le'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frobeniusIsBoundedSMul 📖	mathematical	—	IsBoundedSMul Matrix SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace frobeniusSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	PiLp.isBoundedSMulSeminormedAddCommGroupToPi Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal
frobeniusNormSMulClass 📖	mathematical	—	NormSMulClass Matrix SeminormedRing.toNorm SeminormedAddCommGroup.toNorm frobeniusSeminormedAddCommGroup smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	PiLp.normSMulClassSeminormedAddCommGroupToPi Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal
frobenius_nnnorm_conjTranspose 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	frobenius_nnnorm_map_eq nnnorm_star frobenius_nnnorm_transpose
frobenius_nnnorm_def 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup NNReal Real NNReal.instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal PiLp.nnnorm_eq_of_L2 Finset.sum_congr NNReal.sq_sqrt NNReal.sqrt_eq_rpow NNReal.rpow_two
frobenius_nnnorm_diagonal 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup diagonal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.seminormedAddCommGroup fact_one_le_two_ennreal WithLp.toLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal frobenius_nnnorm_def PiLp.nnnorm_eq_of_L2 Finset.sum_congr Finset.sum_subset Finset.subset_univ Iff.not Finset.mem_map Finset.mem_univ diagonal_apply_ne nnnorm_zero NNReal.zero_rpow two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike Finset.sum_map NNReal.sqrt_eq_rpow diagonal_apply_eq NNReal.rpow_two
frobenius_nnnorm_map_eq 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	Matrix frobeniusSeminormedAddCommGroup map	—	Nat.instAtLeastTwoHAddOfNat frobenius_nnnorm_def Finset.sum_congr
frobenius_nnnorm_mul 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	Nat.instAtLeastTwoHAddOfNat frobenius_nnnorm_def Finset.sum_congr NNReal.mul_rpow Finset.sum_comm Finset.sum_mul_sum NNReal.rpow_le_rpow Finset.sum_le_sum NNReal.addLeftMono NNReal.rpow_le_rpow_iff one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing NNReal.rpow_mul mul_div_cancel₀ two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike NNReal.rpow_one NNReal.rpow_two fact_one_le_two_ennreal RCLike.inner_apply' star_star PiLp.nnnorm_eq_of_L2 nnnorm_star CStarRing.to_normedStarGroup RCLike.instCStarRing NNReal.sqrt_eq_rpow nnnorm_inner_le_nnnorm le_of_lt div_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo
frobenius_nnnorm_one 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup one NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instFunLikeOrderIso NNReal.sqrt AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal frobenius_nnnorm_diagonal PiLp.nnnorm_toLp_const ENNReal.ofNat_ne_top one_div ENNReal.toReal_inv ENNReal.toReal_ofNat NNReal.sqrt_eq_rpow
frobenius_nnnorm_replicateCol 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup Unique.fintype replicateCol WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.seminormedAddCommGroup fact_one_le_two_ennreal WithLp.toLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal frobenius_norm_replicateCol
frobenius_nnnorm_replicateRow 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup Unique.fintype replicateRow WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.seminormedAddCommGroup fact_one_le_two_ennreal WithLp.toLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal frobenius_norm_replicateRow
frobenius_nnnorm_transpose 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup frobeniusSeminormedAddCommGroup transpose	—	Nat.instAtLeastTwoHAddOfNat frobenius_nnnorm_def Finset.sum_comm Finset.sum_congr
frobenius_norm_conjTranspose 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm frobeniusSeminormedAddCommGroup conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	frobenius_nnnorm_conjTranspose
frobenius_norm_def 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm frobeniusSeminormedAddCommGroup Real Real.instPow Finset.sum Real.instAddCommMonoid Finset.univ instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	Nat.instAtLeastTwoHAddOfNat frobenius_nnnorm_def Finset.sum_congr NNReal.rpow_ofNat one_div NNReal.coe_sum Real.rpow_ofNat
frobenius_norm_diagonal 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm frobeniusSeminormedAddCommGroup diagonal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.instNorm WithLp.toLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal frobenius_nnnorm_diagonal
frobenius_norm_map_eq 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm	Matrix frobeniusSeminormedAddCommGroup map	—	frobenius_nnnorm_map_eq
frobenius_norm_mul 📖	mathematical	—	Real Real.instLE Norm.norm Matrix NormedAddCommGroup.toNorm frobeniusNormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instMul	—	frobenius_nnnorm_mul
frobenius_norm_replicateCol 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm frobeniusSeminormedAddCommGroup Unique.fintype replicateCol WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.instNorm WithLp.toLp	—	Nat.instAtLeastTwoHAddOfNat frobenius_norm_def Finset.sum_congr Finset.univ_unique Real.rpow_ofNat Finset.sum_const Finset.card_singleton one_smul one_div PiLp.norm_eq_of_L2 Real.sqrt_eq_rpow
frobenius_norm_replicateRow 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm frobeniusSeminormedAddCommGroup Unique.fintype replicateRow WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.instNorm WithLp.toLp	—	Nat.instAtLeastTwoHAddOfNat frobenius_norm_def Fintype.sum_unique PiLp.norm_eq_of_L2 Real.sqrt_eq_rpow Finset.sum_congr Real.rpow_two
frobenius_norm_transpose 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm frobeniusSeminormedAddCommGroup transpose	—	frobenius_nnnorm_transpose
frobenius_normedStarGroup 📖	mathematical	—	NormedStarGroup Matrix frobeniusSeminormedAddCommGroup instStarAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SeminormedAddCommGroup.toAddCommGroup	—	le_of_eq frobenius_norm_conjTranspose
instNormOneClassOfNonempty 📖	mathematical	—	NormOneClass Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup one NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	norm_diagonal NormOneClass.norm_one Pi.normOneClass
instNormedStarGroup 📖	mathematical	—	NormedStarGroup Matrix seminormedAddCommGroup instStarAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	le_of_eq norm_conjTranspose
isBoundedSMul 📖	mathematical	—	IsBoundedSMul Matrix SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace seminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Pi.instIsBoundedSMul
linftyOpIsBoundedSMul 📖	mathematical	—	IsBoundedSMul Matrix SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace linftyOpSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	fact_one_le_one_ennreal Pi.instIsBoundedSMul PiLp.isBoundedSMulSeminormedAddCommGroupToPi
linftyOpNormSMulClass 📖	mathematical	—	NormSMulClass Matrix SeminormedRing.toNorm SeminormedAddCommGroup.toNorm linftyOpSeminormedAddCommGroup smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	fact_one_le_one_ennreal Pi.instNormSMulClass PiLp.normSMulClassSeminormedAddCommGroupToPi
linfty_opNNNorm_def 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup linftyOpSeminormedAddCommGroup Finset.sup NNReal instSemilatticeSupNNReal NNReal.instOrderBot Finset.univ Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	linfty_opNorm_def
linfty_opNNNorm_diagonal 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup linftyOpSeminormedAddCommGroup diagonal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.seminormedAddGroup	—	linfty_opNNNorm_def Pi.nnnorm_def Finset.sum_eq_single_of_mem Finset.mem_univ diagonal_apply_ne' nnnorm_zero diagonal_apply_eq
linfty_opNNNorm_eq_opNNNorm 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup linftyOpSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField ContinuousLinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule ContinuousLinearMap.toSeminormedAddCommGroup Pi.seminormedAddCommGroup Pi.normedSpace NormedField.toNormedSpace RingHomIsometric.ids mulVecLin	—	RingHomIsometric.ids ContinuousLinearMap.opNNNorm_eq_of_bounds linfty_opNNNorm_mulVec linfty_opNNNorm_def Finset.sup_le isEmpty_or_nonempty Finset.sum_congr Finset.univ_eq_empty NNReal.instCanonicallyOrderedAdd Pi.nnnorm_def Finset.sup_const Finset.univ_nonempty Finset.sup_le_iff mul_one Finset.mem_univ nnnorm_one NormedDivisionRing.to_normOneClass NNReal.nnnorm_eq nnnorm_algebraMap RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
linfty_opNNNorm_mul 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup linftyOpSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	linfty_opNNNorm_def Finset.sum_congr Finset.sup_mono_fun Finset.sum_le_sum NNReal.addLeftMono nnnorm_sum_le_of_le nnnorm_mul_le Finset.sum_comm Finset.mul_sum mul_le_mul_right NNReal.mulLeftMono Finset.le_sup le_refl
linfty_opNNNorm_mulVec 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Matrix linftyOpSeminormedAddCommGroup	—	linfty_opNNNorm_replicateCol linfty_opNNNorm_mul
linfty_opNNNorm_replicateCol 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup linftyOpSeminormedAddCommGroup Unique.fintype replicateCol Pi.seminormedAddGroup	—	linfty_opNNNorm_def Pi.nnnorm_def Finset.sum_congr Finset.univ_unique Finset.sum_const Finset.card_singleton one_smul
linfty_opNNNorm_replicateRow 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup linftyOpSeminormedAddCommGroup Unique.fintype replicateRow Finset.sum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ	—	linfty_opNNNorm_def Finset.univ_unique Finset.sum_congr Finset.sup_singleton
linfty_opNNNorm_toMatrix 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup linftyOpSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix' ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NormedField.toNormedSpace ContinuousLinearMap ContinuousLinearMap.toSeminormedAddCommGroup Pi.seminormedAddCommGroup Pi.normedSpace RingHomIsometric.ids	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass RingHomIsometric.ids linfty_opNNNorm_eq_opNNNorm toLin'_toMatrix'
linfty_opNormOneClass 📖	mathematical	—	NormOneClass Matrix NonUnitalSeminormedRing.toNorm linftyOpNonUnitalSemiNormedRing SeminormedRing.toNonUnitalSeminormedRing one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	linfty_opNorm_diagonal NormOneClass.norm_one Pi.normOneClass
linfty_opNorm_def 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm linftyOpSeminormedAddCommGroup NNReal.toReal Finset.sup NNReal instSemilatticeSupNNReal NNReal.instOrderBot Finset.univ Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	fact_one_le_one_ennreal PiLp.nnnorm_eq_of_L1 Finset.sum_congr
linfty_opNorm_diagonal 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm linftyOpSeminormedAddCommGroup diagonal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.seminormedAddCommGroup	—	fact_one_le_one_ennreal linfty_opNNNorm_diagonal
linfty_opNorm_eq_opNorm 📖	mathematical	—	Norm.norm Matrix NormedAddCommGroup.toNorm linftyOpNormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField ContinuousLinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule ContinuousLinearMap.hasOpNorm Pi.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Pi.normedSpace NormedField.toNormedSpace mulVecLin	—	RingHomIsometric.ids linfty_opNNNorm_eq_opNNNorm
linfty_opNorm_mul 📖	mathematical	—	Real Real.instLE Norm.norm Matrix SeminormedAddCommGroup.toNorm linftyOpSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing NonUnitalNonAssocSemiring.toAddCommMonoid Real.instMul	—	linfty_opNNNorm_mul
linfty_opNorm_mulVec 📖	mathematical	—	Real Real.instLE Norm.norm NonUnitalSeminormedRing.toNorm Pi.nonUnitalSeminormedRing mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing Real.instMul Matrix SeminormedAddCommGroup.toNorm linftyOpSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup	—	linfty_opNNNorm_mulVec
linfty_opNorm_replicateCol 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm linftyOpSeminormedAddCommGroup Unique.fintype replicateCol Pi.seminormedAddCommGroup	—	fact_one_le_one_ennreal linfty_opNNNorm_replicateCol
linfty_opNorm_replicateRow 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm linftyOpSeminormedAddCommGroup Unique.fintype replicateRow Finset.sum Real Real.instAddCommMonoid Finset.univ	—	linfty_opNNNorm_replicateRow NNReal.coe_sum Finset.sum_congr
linfty_opNorm_toMatrix 📖	mathematical	—	Norm.norm Matrix NormedAddCommGroup.toNorm linftyOpNormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix' ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousLinearMap ContinuousLinearMap.hasOpNorm Pi.seminormedAddCommGroup Pi.normedSpace	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass RingHomIsometric.ids linfty_opNNNorm_toMatrix
nnnorm_conjTranspose 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	nnnorm_map_eq nnnorm_star nnnorm_transpose
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup Pi.seminormedAddGroup	—	—
nnnorm_diagonal 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup diagonal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.seminormedAddGroup	—	Pi.nnnorm_def le_antisymm Finset.sup_le eq_or_ne diagonal_apply_eq le_refl diagonal_apply_ne nnnorm_zero zero_le NNReal.instCanonicallyOrderedAdd Eq.trans_le Finset.le_sup Finset.mem_univ
nnnorm_entry_le_entrywise_sup_nnnorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Matrix seminormedAddCommGroup	—	LE.le.trans nnnorm_le_pi_nnnorm
nnnorm_le_iff 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup	—	—
nnnorm_lt_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup	—	pi_nnnorm_lt_iff
nnnorm_map_eq 📖	mathematical	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	Matrix seminormedAddCommGroup map	—	Pi.nnnorm_def
nnnorm_replicateCol 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup Unique.fintype replicateCol Pi.seminormedAddGroup	—	Pi.nnnorm_def Finset.univ_unique Finset.sup_singleton
nnnorm_replicateRow 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup Unique.fintype replicateRow Pi.seminormedAddGroup	—	Pi.nnnorm_def Finset.univ_unique Finset.sup_singleton
nnnorm_transpose 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup transpose	—	Finset.sup_comm
normSMulClass 📖	mathematical	—	NormSMulClass Matrix SeminormedRing.toNorm SeminormedAddCommGroup.toNorm seminormedAddCommGroup smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	Pi.instNormSMulClass
norm_conjTranspose 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	nnnorm_conjTranspose
norm_def 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup Pi.seminormedAddCommGroup	—	—
norm_diagonal 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup diagonal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.seminormedAddCommGroup	—	nnnorm_diagonal
norm_entry_le_entrywise_sup_norm 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Matrix seminormedAddCommGroup	—	LE.le.trans norm_le_pi_norm
norm_eq_sup_sup_nnnorm 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup NNReal.toReal Finset.sup NNReal instSemilatticeSupNNReal NNReal.instOrderBot Finset.univ NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	Pi.nnnorm_def
norm_le_iff 📖	mathematical	Real Real.instLE Real.instZero	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup	—	pi_norm_le_iff_of_nonneg
norm_lt_iff 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup	—	pi_norm_lt_iff
norm_map_eq 📖	mathematical	Norm.norm SeminormedAddCommGroup.toNorm	Matrix seminormedAddCommGroup map	—	nnnorm_map_eq
norm_replicateCol 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup Unique.fintype replicateCol Pi.seminormedAddCommGroup	—	nnnorm_replicateCol
norm_replicateRow 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup Unique.fintype replicateRow Pi.seminormedAddCommGroup	—	nnnorm_replicateRow
norm_transpose 📖	mathematical	—	Norm.norm Matrix SeminormedAddCommGroup.toNorm seminormedAddCommGroup transpose	—	nnnorm_transpose

---

← Back to Index