SchurComplement

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

Statistics

Metric	Count
Definitions `fromBlocksZero₁₂Invertible`, `fromBlocksZero₁₂InvertibleEquiv`, `fromBlocksZero₂₁Invertible`, `fromBlocksZero₂₁InvertibleEquiv`, `fromBlocks₁₁Invertible`, `fromBlocks₂₂Invertible`, `invertibleEquivFromBlocks₁₁Invertible`, `invertibleEquivFromBlocks₂₂Invertible`, `invertibleOfFromBlocksZero₁₂Invertible`, `invertibleOfFromBlocksZero₂₁Invertible`, `invertibleOfFromBlocks₁₁Invertible`, `invertibleOfFromBlocks₂₂Invertible`	12
Theorems `det_add_mul`, `det_add_replicateCol_mul_replicateRow`, `det_fromBlocks_one₁₁`, `det_fromBlocks_one₂₂`, `det_fromBlocks₁₁`, `det_fromBlocks₂₂`, `det_mul_add_one_comm`, `det_one_add_mul_comm`, `det_one_add_replicateCol_mul_replicateRow`, `det_one_sub_mul_comm`, `fromBlocks_eq_of_invertible₁₁`, `fromBlocks_eq_of_invertible₂₂`, `invOf_fromBlocks_zero₁₂_eq`, `invOf_fromBlocks_zero₂₁_eq`, `invOf_fromBlocks₁₁_eq`, `invOf_fromBlocks₂₂_eq`, `inv_fromBlocks_zero₁₂_of_isUnit_iff`, `inv_fromBlocks_zero₂₁_of_isUnit_iff`, `isUnit_fromBlocks_iff_of_invertible₁₁`, `isUnit_fromBlocks_iff_of_invertible₂₂`, `isUnit_fromBlocks_zero₁₂`, `isUnit_fromBlocks_zero₂₁`	22
Total	34

Matrix

Definitions

Name	Category	Theorems
`fromBlocksZero₁₂Invertible` 📖	CompOp	—
`fromBlocksZero₁₂InvertibleEquiv` 📖	CompOp	—
`fromBlocksZero₂₁Invertible` 📖	CompOp	—
`fromBlocksZero₂₁InvertibleEquiv` 📖	CompOp	—
`fromBlocks₁₁Invertible` 📖	CompOp	—
`fromBlocks₂₂Invertible` 📖	CompOp	—
`invertibleEquivFromBlocks₁₁Invertible` 📖	CompOp	—
`invertibleEquivFromBlocks₂₂Invertible` 📖	CompOp	—
`invertibleOfFromBlocksZero₁₂Invertible` 📖	CompOp	—
`invertibleOfFromBlocksZero₂₁Invertible` 📖	CompOp	—
`invertibleOfFromBlocks₁₁Invertible` 📖	CompOp	—
`invertibleOfFromBlocks₂₂Invertible` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_add_mul` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `det`	`Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `inv`	—	`mul_one` `mul_nonsing_inv_cancel_left` `mul_add` `det_mul` `mul_assoc` `det_one_add_mul_comm`
`det_add_replicateCol_mul_replicateRow` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `det`	`Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Unique.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `replicateCol` `replicateRow` `decidableEq_of_subsingleton` `Unique.instSubsingleton` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `inv`	—	`Unique.instSubsingleton` `mul_one` `mul_nonsing_inv_cancel_left` `mul_add` `det_mul` `mul_assoc` `det_one_add_mul_comm`
`det_fromBlocks_one₁₁` 📖	mathematical	—	`det` `instFintypeSum` `fromBlocks` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`det_fromBlocks₁₁` `invOf_one` `mul_one` `det_one` `one_mul`
`det_fromBlocks_one₂₂` 📖	mathematical	—	`det` `instFintypeSum` `fromBlocks` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`det_fromBlocks₂₂` `invOf_one` `mul_one` `det_one` `one_mul`
`det_fromBlocks₁₁` 📖	mathematical	—	`det` `instFintypeSum` `fromBlocks` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`fromBlocks_eq_of_invertible₁₁` `det_mul` `det_fromBlocks_zero₂₁` `det_fromBlocks_zero₁₂` `det_one` `one_mul` `mul_one`
`det_fromBlocks₂₂` 📖	mathematical	—	`det` `instFintypeSum` `fromBlocks` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`ext` `det_submatrix_equiv_self` `det_fromBlocks₁₁`
`det_mul_add_one_comm` 📖	mathematical	—	`det` `Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`add_comm` `det_one_add_mul_comm`
`det_one_add_mul_comm` 📖	mathematical	—	`det` `Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`det_fromBlocks_one₂₂` `neg_mul` `sub_neg_eq_add` `det_fromBlocks_one₁₁` `mul_neg`
`det_one_add_replicateCol_mul_replicateRow` 📖	mathematical	—	`det` `Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Unique.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `replicateCol` `replicateRow` `dotProduct`	—	`Unique.instSubsingleton` `det_one_add_mul_comm` `det_unique` `Pi.add_apply` `one_apply_eq` `replicateRow_mul_replicateCol_apply`
`det_one_sub_mul_comm` 📖	mathematical	—	`det` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`sub_eq_add_neg` `neg_mul` `det_one_add_mul_comm` `mul_neg`
`fromBlocks_eq_of_invertible₁₁` 📖	mathematical	—	`fromBlocks` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `zero` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`mul_assoc` `fromBlocks_multiply` `one_mul` `mul_zero` `add_zero` `zero_mul` `invOf_mul_self` `mul_one` `zero_add` `mul_invOf_cancel_left` `add_sub_cancel`
`fromBlocks_eq_of_invertible₂₂` 📖	mathematical	—	`fromBlocks` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `zero` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`Equiv.injective` `fromBlocks_submatrix_sum_swap_right` `fromBlocks_submatrix_sum_swap_left` `submatrix_id_id` `invOf_eq_nonsing_inv` `submatrix_mul_equiv` `fromBlocks_eq_of_invertible₁₁`
`invOf_fromBlocks_zero₁₂_eq` 📖	mathematical	—	`Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `fromBlocks` `zero` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instHMulOfFintypeOfMulOfAddCommMonoid`	—	`Invertible.congr`
`invOf_fromBlocks_zero₂₁_eq` 📖	mathematical	—	`Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `fromBlocks` `zero` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instHMulOfFintypeOfMulOfAddCommMonoid`	—	`Invertible.congr`
`invOf_fromBlocks₁₁_eq` 📖	mathematical	—	`Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `fromBlocks` `add` `Distrib.toAdd` `instHMulOfFintypeOfMulOfAddCommMonoid` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`Invertible.congr`
`invOf_fromBlocks₂₂_eq` 📖	mathematical	—	`Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `fromBlocks` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `instHMulOfFintypeOfMulOfAddCommMonoid` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `add` `Distrib.toAdd`	—	`Invertible.congr`
`inv_fromBlocks_zero₁₂_of_isUnit_iff` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`inv` `instFintypeSum` `fromBlocks` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`IsUnit.nonempty_invertible` `invOf_fromBlocks_zero₁₂_eq` `Iff.not` `isUnit_fromBlocks_zero₁₂` `nonsing_inv_eq_ringInverse` `Ring.inverse_non_unit` `zero_mul` `neg_zero` `fromBlocks_zero`
`inv_fromBlocks_zero₂₁_of_isUnit_iff` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`inv` `instFintypeSum` `fromBlocks` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`IsUnit.nonempty_invertible` `invOf_fromBlocks_zero₂₁_eq` `Iff.not` `isUnit_fromBlocks_zero₂₁` `nonsing_inv_eq_ringInverse` `Ring.inverse_non_unit` `zero_mul` `neg_zero` `fromBlocks_zero`
`isUnit_fromBlocks_iff_of_invertible₁₁` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFintypeSum` `fromBlocks` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Equiv.nonempty_congr`
`isUnit_fromBlocks_iff_of_invertible₂₂` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFintypeSum` `fromBlocks` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Equiv.nonempty_congr`
`isUnit_fromBlocks_zero₁₂` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFintypeSum` `fromBlocks` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Equiv.nonempty_congr`
`isUnit_fromBlocks_zero₂₁` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFintypeSum` `fromBlocks` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Equiv.nonempty_congr`

---

← Back to Index