Adjugate

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

Statistics

Metric	Count
Definitions `adjugate`, `cramer`, `cramerMap`	3
Theorems `map_adjugate`, `adjugate`, `adjugate_adjugate`, `adjugate_adjugate'`, `adjugate_apply`, `adjugate_conjTranspose`, `adjugate_def`, `adjugate_diagonal`, `adjugate_eq_one_of_card_eq_one`, `adjugate_fin_one`, `adjugate_fin_succ_eq_det_submatrix`, `adjugate_fin_three`, `adjugate_fin_three_of`, `adjugate_fin_two`, `adjugate_fin_two_of`, `adjugate_fin_zero`, `adjugate_mul`, `adjugate_mul_distrib`, `adjugate_mul_distrib_aux`, `adjugate_one`, `adjugate_pow`, `adjugate_reindex`, `adjugate_smul`, `adjugate_submatrix_equiv_self`, `adjugate_subsingleton`, `adjugate_transpose`, `adjugate_zero`, `cramerMap_is_linear`, `cramer_apply`, `cramer_eq_adjugate_mulVec`, `cramer_is_linear`, `cramer_one`, `cramer_reindex`, `cramer_row_self`, `cramer_smul`, `cramer_submatrix_equiv`, `cramer_subsingleton_apply`, `cramer_transpose_apply`, `cramer_transpose_row_self`, `cramer_zero`, `det_adjugate`, `det_eq_sum_mul_adjugate_col`, `det_eq_sum_mul_adjugate_row`, `det_smul_adjugate_adjugate`, `isRegular_of_isLeftRegular_det`, `mulVec_cramer`, `mul_adjugate`, `mul_adjugate_apply`, `sum_cramer`, `sum_cramer_apply`, `map_adjugate`	51
Total	54

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_adjugate` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Matrix` `Matrix.semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.instAlgebra` `funLike` `mapMatrix` `Matrix.adjugate`	—	`RingHom.map_adjugate`

Matrix

Definitions

Name	Category	Theorems
`adjugate` 📖	CompOp	42 math math: `adjugate_fin_two`, `adjugate_fin_succ_eq_det_submatrix`, `det_eq_sum_mul_adjugate_row`, `Continuous.matrix_adjugate`, `adjugate_fin_one`, `adjugate_fin_three`, `det_eq_sum_mul_adjugate_col`, `adjugate_mul_distrib_aux`, `adjugate_adjugate`, `AlgHom.map_adjugate`, `inv_def`, `adjugate_conjTranspose`, `adjugate_fin_three_of`, `adjugate_eq_one_of_card_eq_one`, `adjugate_reindex`, `adjugate_apply`, `inv_adjugate`, `mul_adjugate_apply`, `adjugate_diagonal`, `adjugate_smul`, `nonsing_inv_apply`, `adjugate_mul_distrib`, `adjugate_adjugate'`, `SpecialLinearGroup.coe_inv`, `det_adjugate`, `adjugate_def`, `RingHom.map_adjugate`, `det_smul_adjugate_adjugate`, `adjugate_zero`, `adjugate_submatrix_equiv_self`, `adjugate_subsingleton`, `adjugate_one`, `IsSymm.adjugate`, `adjugate_transpose`, `IsHermitian.adjugate`, `adjugate_fin_zero`, `invOf_eq`, `adjugate_pow`, `adjugate_mul`, `adjugate_fin_two_of`, `cramer_eq_adjugate_mulVec`, `mul_adjugate`
`cramer` 📖	CompOp	20 math math: `det_smul_inv_mulVec_eq_cramer`, `cramer_transpose_row_self`, `cramer_row_self`, `sum_cramer`, `cramer_apply`, `cramer_zero`, `cramer_reindex`, `AffineBasis.det_smul_coords_eq_cramer_coords`, `mul_adjugate_apply`, `sum_cramer_apply`, `adjugate_def`, `cramer_submatrix_equiv`, `cramer_subsingleton_apply`, `Continuous.matrix_cramer`, `mulVec_cramer`, `cramer_one`, `cramer_smul`, `cramer_transpose_apply`, `cramer_eq_adjugate_mulVec`, `det_smul_inv_vecMul_eq_cramer_transpose`
`cramerMap` 📖	CompOp	2 math math: `cramer_is_linear`, `cramerMap_is_linear`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjugate_adjugate` 📖	mathematical	—	`adjugate` `Matrix` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `det` `Fintype.card`	—	`subsingleton_of_empty_right` `Fintype.card_eq_zero_iff` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `MvPolynomial.instIsCancelMulZeroOfIsCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Int.instIsCancelMulZero` `det_mvPolynomialX_ne_zero` `Int.instNontrivial` `IsSMulRegular.matrix` `smul_smul` `pow_succ'` `det_smul_adjugate_adjugate` `mvPolynomialX_mapMatrix_aeval` `AlgHom.map_adjugate` `AlgHom.map_det` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.mapMatrix_apply` `map_smul'` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass`
`adjugate_adjugate'` 📖	mathematical	—	`adjugate` `Matrix` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `det` `Fintype.card`	—	`adjugate_adjugate` `LT.lt.ne'` `Fintype.one_lt_card`
`adjugate_apply` 📖	mathematical	—	`adjugate` `det` `updateRow` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`adjugate_def` `of_apply` `cramer_apply` `updateCol_transpose` `det_transpose`
`adjugate_conjTranspose` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `adjugate`	—	`RingHom.map_adjugate` `adjugate_transpose`
`adjugate_def` 📖	mathematical	—	`adjugate` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `transpose` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`adjugate_diagonal` 📖	mathematical	—	`adjugate` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.prod` `CommRing.toCommMonoid` `Finset.erase` `Finset.univ`	—	`ext` `diagonal_transpose` `eq_or_ne` `diagonal_apply_eq` `diagonal_updateCol_single` `det_diagonal` `Finset.prod_update_of_mem` `Finset.mem_univ` `Finset.sdiff_singleton_eq_erase` `one_mul` `diagonal_apply_ne` `det_eq_zero_of_row_eq_zero` `updateCol_self` `Pi.single_eq_of_ne'` `updateCol_ne` `diagonal_apply_ne'`
`adjugate_eq_one_of_card_eq_one` 📖	mathematical	`Fintype.card`	`adjugate` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`adjugate_subsingleton` `Fintype.card_le_one_iff_subsingleton` `Eq.le`
`adjugate_fin_one` 📖	mathematical	—	`adjugate` `Fin.fintype` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`adjugate_subsingleton`
`adjugate_fin_succ_eq_det_submatrix` 📖	mathematical	—	`adjugate` `Fin.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `det` `submatrix` `Fin.succAbove`	—	`adjugate_apply` `det_succ_row` `Finset.sum_congr` `updateRow_self` `det.congr_simp` `submatrix_updateRow_succAbove` `Fintype.sum_eq_single` `Pi.single_eq_of_ne` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Pi.single_eq_same` `mul_one`
`adjugate_fin_three` 📖	mathematical	—	`adjugate` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `vecEmpty`	—	`ext` `adjugate_fin_succ_eq_det_submatrix` `det_fin_two` `Fintype.complete` `add_zero` `pow_zero` `one_mul` `cons_val'` `cons_val_fin_one` `pow_one` `Nat.instZeroLEOneClass` `neg_mul` `neg_sub` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Even.neg_pow` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instCharZero` `zero_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Meta.NormNum.isInt_pow` `Mathlib.Meta.NormNum.intPow_negOfNat_bit1` `Mathlib.Meta.NormNum.one_natPow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.intPow_negOfNat_bit0`
`adjugate_fin_three_of` 📖	mathematical	—	`adjugate` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`adjugate_fin_three`
`adjugate_fin_two` 📖	mathematical	—	`adjugate` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `vecEmpty`	—	`ext` `adjugate_fin_succ_eq_det_submatrix` `Fintype.complete` `add_zero` `pow_zero` `det_unique` `one_mul` `cons_val'` `cons_val_fin_one` `pow_one` `Fin.succAbove_ne_zero_zero` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `neg_mul` `zero_add` `Even.neg_pow` `Nat.instAtLeastTwoHAddOfNat` `one_pow`
`adjugate_fin_two_of` 📖	mathematical	—	`adjugate` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`adjugate_fin_two`
`adjugate_fin_zero` 📖	mathematical	—	`adjugate` `Fin.fintype` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`subsingleton_of_empty_right` `Fin.isEmpty'`
`adjugate_mul` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjugate` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `det` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`adjugate_transpose` `transpose_mul` `transpose_transpose` `mul_adjugate` `det_transpose` `transpose_smul` `transpose_one`
`adjugate_mul_distrib` 📖	mathematical	—	`adjugate` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`ext` `Polynomial.eval_add` `Polynomial.eval_C` `Polynomial.eval_mul` `Polynomial.eval_X` `MulZeroClass.zero_mul` `add_zero` `RingHom.map_adjugate` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Polynomial.Monic.isRegular` `det.congr_simp` `add_comm` `Polynomial.leadingCoeff_det_X_one_add_C` `RingHom.map_mul` `adjugate_mul_distrib_aux` `IsRegular.left`
`adjugate_mul_distrib_aux` 📖	mathematical	`IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `det`	`adjugate` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`det_mul` `IsLeftRegular.mul` `IsRegular.left` `isRegular_of_isLeftRegular_det` `mul_adjugate` `mul_assoc` `smul_mul` `IsScalarTower.right` `one_mul` `mul_smul` `Algebra.to_smulCommClass` `smul_smul` `mul_comm`
`adjugate_one` 📖	mathematical	—	`adjugate` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`ext` `transpose_one` `cramer_one` `Pi.single_apply`
`adjugate_pow` 📖	mathematical	—	`adjugate` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`pow_zero` `adjugate_one` `pow_succ'` `adjugate_mul_distrib` `pow_succ`
`adjugate_reindex` 📖	mathematical	—	`adjugate` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	`adjugate_submatrix_equiv_self`
`adjugate_smul` 📖	mathematical	—	`adjugate` `Matrix` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card`	—	`adjugate.eq_1` `transpose_smul` `Function.smulCommClass` `Algebra.to_smulCommClass` `cramer_smul`
`adjugate_submatrix_equiv_self` 📖	mathematical	—	`adjugate` `submatrix` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`ext` `Function.update_comp_equiv` `adjugate_apply` `submatrix_apply` `det_submatrix_equiv_self` `updateRow_submatrix_equiv`
`adjugate_subsingleton` 📖	mathematical	—	`adjugate` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`ext` `adjugate.congr_simp` `adjugate_apply` `det_eq_elem_of_subsingleton` `updateRow.congr_simp` `updateRow_self` `Pi.single_eq_same`
`adjugate_transpose` 📖	mathematical	—	`transpose` `adjugate`	—	`ext` `transpose_apply` `adjugate_apply` `updateRow_transpose` `det_transpose` `det_apply'` `Finset.sum_congr` `Equiv.injective` `updateRow_apply` `updateCol_apply` `Pi.single_eq_same` `Finset.prod_eq_zero` `Finset.mem_univ` `updateCol_self` `Pi.single_eq_of_ne'` `updateRow.congr_simp` `Equiv.apply_symm_apply` `updateRow_self` `Pi.single_eq_of_ne` `Equiv.symm_apply_eq`
`adjugate_zero` 📖	mathematical	—	`adjugate` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`ext` `exists_ne` `det_eq_zero_of_column_eq_zero` `updateCol_ne`
`cramerMap_is_linear` 📖	mathematical	—	`IsLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `cramerMap`	—	`det_updateCol_add` `det_updateCol_smul`
`cramer_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `det` `updateCol`	—	—
`cramer_eq_adjugate_mulVec` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `mulVec` `adjugate`	—	`transpose_transpose` `adjugate_transpose` `adjugate_def` `pi_eq_sum_univ` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Pi.single_apply` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Finset.sum_apply` `mul_comm`
`cramer_is_linear` 📖	mathematical	—	`IsLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `cramerMap`	—	`IsLinearMap.map_add` `cramerMap_is_linear` `IsLinearMap.map_smul`
`cramer_one` 📖	mathematical	—	`cramer` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `Module.End.instOne`	—	`LinearMap.pi_ext'` `Finite.of_fintype` `LinearMap.ext_ring` `RingHomCompTriple.ids` `det_one` `cramer_row_self` `one_eq_pi_single` `Pi.single_comm`
`cramer_reindex` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.symm`	—	`cramer_submatrix_equiv`
`cramer_row_self` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `det`	—	`transpose_transpose` `det_transpose` `cramer_transpose_row_self`
`cramer_smul` 📖	mathematical	—	`cramer` `Matrix` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instSMul` `Pi.distribSMul` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NonUnitalNonAssocSemiring.toDistribSMul` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `Algebra.to_smulCommClass` `Monoid.toNatPow` `Fintype.card`	—	`LinearMap.ext` `Function.smulCommClass` `Algebra.to_smulCommClass` `det_updateCol_smul_left`
`cramer_submatrix_equiv` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `submatrix` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`det.congr_simp` `updateCol_submatrix_equiv` `det_submatrix_equiv_self`
`cramer_subsingleton_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer`	—	`cramer_apply` `det_eq_elem_of_subsingleton` `updateCol_self`
`cramer_transpose_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `transpose` `det` `updateRow`	—	`cramer_apply` `updateCol_transpose` `det_transpose`
`cramer_transpose_row_self` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `transpose` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `det`	—	`cramer_apply` `Pi.single_apply` `det.congr_simp` `updateCol_transpose` `updateRow_eq_self` `det_transpose` `det_zero_of_row_eq` `updateRow_self` `updateRow_ne`
`cramer_zero` 📖	mathematical	—	`cramer` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instZero`	—	`LinearMap.pi_ext'` `Finite.of_fintype` `LinearMap.ext_ring` `RingHomCompTriple.ids` `exists_ne` `det_eq_zero_of_column_eq_zero` `updateCol_ne`
`det_adjugate` 📖	mathematical	—	`det` `adjugate` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Fintype.card`	—	`pow_zero` `adjugate_subsingleton` `IsEmpty.instSubsingleton` `Fintype.card_eq_zero_iff` `det_one` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LT.lt.nat_succ_le` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `MvPolynomial.instIsCancelMulZeroOfIsCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Int.instIsCancelMulZero` `det_mvPolynomialX_ne_zero` `Int.instNontrivial` `det_mul` `mul_adjugate` `det_smul` `mul_one` `pow_succ'` `mvPolynomialX_mapMatrix_aeval` `AlgHom.map_adjugate` `AlgHom.map_det` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`det_eq_sum_mul_adjugate_col` 📖	mathematical	—	`det` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `adjugate`	—	`det_transpose` `Finset.sum_congr` `det_eq_sum_mul_adjugate_row`
`det_eq_sum_mul_adjugate_row` 📖	mathematical	—	`det` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `adjugate`	—	`Fintype.card_ne_zero` `det_succ_row` `Finset.sum_congr` `mul_assoc` `mul_left_comm` `Equiv.symm_apply_apply` `adjugate.congr_simp` `Equiv.sum_comp` `adjugate_reindex` `det_reindex_self`
`det_smul_adjugate_adjugate` 📖	mathematical	—	`Matrix` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `det` `adjugate` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card`	—	`adjugate_mul_distrib` `adjugate_mul` `adjugate_smul` `adjugate_one` `one_mul` `smul_mul` `IsScalarTower.right` `mul_one` `mul_smul` `Algebra.to_smulCommClass` `mul_adjugate` `mul_assoc`
`isRegular_of_isLeftRegular_det` 📖	mathematical	`IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `det`	`IsRegular` `Matrix` `instMulOfFintypeOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`IsLeftRegular.matrix` `one_mul` `smul_mul` `IsScalarTower.right` `adjugate_mul` `mul_assoc` `mul_one` `mul_smul` `Algebra.to_smulCommClass` `mul_adjugate`
`mulVec_cramer` 📖	mathematical	—	`mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `Function.hasSMul` `Algebra.toSMul` `Algebra.id` `det`	—	`cramer_eq_adjugate_mulVec` `mulVec_mulVec` `mul_adjugate` `smul_mulVec` `IsScalarTower.right` `one_mulVec`
`mul_adjugate` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjugate` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `det` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`ext` `mul_apply` `Pi.smul_apply` `one_apply` `smul_eq_mul` `mul_boole` `Finset.sum_congr` `mul_adjugate_apply` `sum_cramer_apply` `Pi.single_apply` `Finset.sum_ite_eq` `cramer_transpose_row_self`
`mul_adjugate_apply` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `adjugate` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer` `transpose` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`smul_eq_mul` `adjugate.eq_1` `of_apply` `Pi.smul_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Pi.single_smul'` `mul_one`
`sum_cramer` 📖	mathematical	—	`Finset.sum` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`sum_cramer_apply` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `cramer`	—	`Finset.sum_apply` `sum_cramer` `cramer_apply`

Matrix.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjugate` 📖	mathematical	`Matrix.IsSymm`	`Matrix.adjugate`	—	`eq_1` `Matrix.adjugate_transpose` `eq`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_adjugate` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Matrix` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike` `mapMatrix` `Matrix.adjugate`	—	`Matrix.ext` `map_one` `Pi.single_op` `map_zero` `Matrix.adjugate_apply` `mapMatrix_apply` `Matrix.map_apply` `Matrix.map_updateRow` `map_det`

---

← Back to Index