Documentation Verification Report

IsDiag

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

Statistics

Metric	Count
Definitions `IsDiag`, `IsDiag`	2
Theorems `add`, `conjTranspose`, `diagonal_diag`, `fromBlocks`, `fromBlocks_of_isSymm`, `isSymm`, `kronecker`, `map`, `neg`, `smul`, `sub`, `submatrix`, `transpose`, `isDiag_conjTranspose_iff`, `isDiag_diagonal`, `isDiag_fromBlocks_iff`, `isDiag_iff_diagonal_diag`, `isDiag_neg_iff`, `isDiag_of_subsingleton`, `isDiag_one`, `isDiag_smul_one`, `isDiag_transpose_iff`, `isDiag_zero`, `mul_transpose_self_isDiag_iff_hasOrthogonalRows`, `transpose_mul_self_isDiag_iff_hasOrthogonalCols`	25
Total	27

Matrix

Definitions

Name	Category	Theorems
`IsDiag` 📖	MathDef	12 math math: `isDiag_one`, `isDiag_neg_iff`, `isDiag_conjTranspose_iff`, `isDiag_of_subsingleton`, `isDiag_smul_one`, `mul_transpose_self_isDiag_iff_hasOrthogonalRows`, `isDiag_diagonal`, `isDiag_fromBlocks_iff`, `isDiag_iff_diagonal_diag`, `transpose_mul_self_isDiag_iff_hasOrthogonalCols`, `isDiag_zero`, `isDiag_transpose_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDiag_conjTranspose_iff` 📖	mathematical	—	`IsDiag` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`conjTranspose_conjTranspose` `IsDiag.conjTranspose`
`isDiag_diagonal` 📖	mathematical	—	`IsDiag` `diagonal`	—	`diagonal_apply_ne`
`isDiag_fromBlocks_iff` 📖	mathematical	—	`IsDiag` `fromBlocks` `Matrix` `zero`	—	`Sum.inl_injective` `ext` `Sum.inr_injective` `IsDiag.fromBlocks`
`isDiag_iff_diagonal_diag` 📖	mathematical	—	`IsDiag` `diagonal` `diag`	—	`IsDiag.diagonal_diag` `isDiag_diagonal`
`isDiag_neg_iff` 📖	mathematical	—	`IsDiag` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `Matrix` `neg` `NegZeroClass.toNeg`	—	`neg_eq_zero` `IsDiag.neg`
`isDiag_of_subsingleton` 📖	mathematical	—	`IsDiag`	—	—
`isDiag_one` 📖	mathematical	—	`IsDiag` `Matrix` `one`	—	`one_apply_ne`
`isDiag_smul_one` 📖	mathematical	—	`IsDiag` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `Matrix` `smul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero` `one` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`IsDiag.smul` `isDiag_one`
`isDiag_transpose_iff` 📖	mathematical	—	`IsDiag` `transpose`	—	`IsDiag.transpose`
`isDiag_zero` 📖	mathematical	—	`IsDiag` `Matrix` `zero`	—	—
`mul_transpose_self_isDiag_iff_hasOrthogonalRows` 📖	mathematical	—	`IsDiag` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `transpose` `HasOrthogonalRows`	—	—
`transpose_mul_self_isDiag_iff_hasOrthogonalCols` 📖	mathematical	—	`IsDiag` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `transpose` `HasOrthogonalCols`	—	—

Matrix.IsDiag

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Matrix.IsDiag` `AddZero.toZero` `AddZeroClass.toAddZero`	`Matrix` `Matrix.add` `AddZero.toAdd`	—	`add_zero`
`conjTranspose` 📖	mathematical	`Matrix.IsDiag` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`map` `transpose` `star_zero`
`diagonal_diag` 📖	mathematical	`Matrix.IsDiag`	`Matrix.diagonal` `Matrix.diag`	—	`Matrix.ext` `Decidable.eq_or_ne` `Matrix.diagonal_apply_eq` `Matrix.diag.eq_1` `Matrix.diagonal_apply_ne`
`fromBlocks` 📖	mathematical	`Matrix.IsDiag`	`Matrix.fromBlocks` `Matrix` `Matrix.zero`	—	—
`fromBlocks_of_isSymm` 📖	—	`Matrix.IsSymm` `Matrix.fromBlocks` `Matrix` `Matrix.zero` `Matrix.IsDiag`	—	—	`Matrix.isSymm_fromBlocks_iff` `fromBlocks`
`isSymm` 📖	mathematical	`Matrix.IsDiag`	`Matrix.IsSymm`	—	`Matrix.ext` `Matrix.transpose_apply`
`kronecker` 📖	mathematical	`Matrix.IsDiag` `MulZeroClass.toZero`	`Matrix.kroneckerMap` `MulZeroClass.toMul`	—	`MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`map` 📖	mathematical	`Matrix.IsDiag`	`Matrix.map`	—	—
`neg` 📖	mathematical	`Matrix.IsDiag` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`Matrix` `Matrix.neg` `NegZeroClass.toNeg`	—	`neg_zero`
`smul` 📖	mathematical	`Matrix.IsDiag`	`Matrix` `Matrix.smul` `SMulZeroClass.toSMul`	—	`smul_zero`
`sub` 📖	mathematical	`Matrix.IsDiag` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`Matrix` `Matrix.sub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	`sub_zero`
`submatrix` 📖	mathematical	`Matrix.IsDiag`	`Matrix.submatrix`	—	—
`transpose` 📖	mathematical	`Matrix.IsDiag`	`Matrix.transpose`	—	—

Sym2

Definitions

Name	Category	Theorems
`IsDiag` 📖	MathDef	27 math math: `card_subtype_not_diag`, `filter_image_mk_isDiag`, `fromRel_ne`, `SimpleGraph.not_isDiag_of_mem_edgeFinset`, `fromRel_irrefl`, `QuadraticMap.map_finsuppSum`, `diagSet_eq_setOf_isDiag`, `diag_isDiag`, `isDiag_iff_mem_range_diag`, `diagSet_compl_eq_setOf_not_isDiag`, `isDiag_iff_proj_eq`, `filter_image_mk_not_isDiag`, `isDiag_of_subsingleton`, `mk_isDiag_iff`, `SimpleGraph.not_isDiag_of_mem_edgeSet`, `card_toFinset`, `QuadraticMap.apply_linearCombination`, `Finset.not_isDiag_mk_of_mem_offDiag`, `card_subtype_diag`, `Finset.sum_sym2_filter_not_isDiag`, `QuadraticMap.map_sum`, `QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar`, `mem_diagSet`, `fromRel_irreflexive`, `isDiag_map`, `mem_diagSet_iff_isDiag`, `Finset.isDiag_mk_of_mem_diag`

---

← Back to Index