Documentation Verification Report

Transitivity

📁 Source: Mathlib/RingTheory/Norm/Transitivity.lean

Statistics

Metric	Count
Definitions `auxMat`, `cornerAddX`, `termMulAuxMatBlock`	3
Theorems `auxMat_blockTriangular`, `auxMat_toSquareBlock_eq`, `auxMat_toSquareBlock_ne`, `comp_det_mul_pow`, `det_det_aux`, `det_mul_corner_pow`, `eval_zero_comp_det`, `eval_zero_det_det`, `mul_auxMat_blockTriangular`, `mul_auxMat_corner`, `mul_auxMat_toSquareBlock_eq`, `polyToMatrix_cornerAddX`, `isIntegral_norm`, `norm_eq_norm_adjoin`, `norm_eq_prod_automorphisms`, `norm_eq_prod_embeddings`, `norm_eq_prod_roots`, `norm_norm`, `det_restrictScalars`, `det_det`	20
Total	23

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegral_norm` 📖	mathematical	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `norm`	—	`IsScalarTower.left` `norm_norm` `Module.Free.of_divisionRing` `IntermediateField.isScalarTower_mid'` `IntermediateField.AdjoinSimple.coe_gen` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.algebraMap_apply` `IntermediateField.finiteDimensional_right` `norm_algebraMap_of_basis` `map_pow` `MonoidHom.instMonoidHomClass` `IsIntegral.pow` `isIntegral_algebraMap_iff` `AlgebraicClosure.instIsScalarTower` `IntermediateField.isScalarTower` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsDomain` `IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots` `IsAlgClosed.splits` `AlgebraicClosure.isAlgClosed` `IsIntegral.multiset_prod` `minpoly.monic` `minpoly.dvd` `Polynomial.aeval_map_algebraMap` `minpoly.aeval` `Polynomial.aeval_mul` `Polynomial.mem_aroots'` `MulZeroClass.zero_mul` `norm_eq_one_of_not_module_finite` `isIntegral_one`
`norm_eq_norm_adjoin` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `norm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `IntermediateField.toField` `IntermediateField.algebra'` `toSMul` `Semifield.toCommSemiring` `id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `toModule` `IntermediateField.AdjoinSimple.gen` `Module.finrank` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`IsScalarTower.left` `IntermediateField.AdjoinSimple.coe_gen` `norm_norm` `Module.Free.of_divisionRing` `IntermediateField.isScalarTower_mid'` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.algebraMap_apply` `IntermediateField.finiteDimensional_right` `norm_algebraMap_of_basis` `map_pow` `MonoidHom.instMonoidHomClass` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `norm_eq_one_of_not_module_finite` `IntermediateField.adjoin.finiteDimensional` `Module.Finite.trans` `Module.finrank_of_not_finite` `pow_zero` `IntermediateField.AdjoinSimple.isIntegral_gen` `IsIntegral.isIntegral` `IsAlgebraic.isIntegral` `IsAlgebraic.of_finite` `one_pow`
`norm_eq_prod_automorphisms` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `norm` `Finset.prod` `AlgEquiv` `CommRing.toCommMonoid` `Finset.univ` `AlgEquiv.fintype` `AlgEquiv.instFunLike`	—	`FaithfulSMul.algebraMap_injective` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `instIsDomain` `Fintype.prod_equiv` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `IsGalois.to_normal` `AlgHom.restrictNormal_commutes` `norm_eq_prod_embeddings` `IsGalois.to_isSeparable` `AlgebraicClosure.isAlgClosed` `IsScalarTower.algebraMap_apply`
`norm_eq_prod_embeddings` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `norm` `Finset.prod` `AlgHom` `CommRing.toCommMonoid` `Finset.univ` `minpoly.AlgHom.fintype` `instIsDomain` `AlgHom.funLike`	—	`IsSeparable.isIntegral` `instIsDomain` `IsScalarTower.left` `norm_eq_norm_adjoin` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IntermediateField.adjoin.powerBasis_gen` `norm_eq_prod_embeddings_gen` `IsAlgClosed.splits` `IsSeparable.isSeparable` `isSeparable_tower_bot_of_isSeparable` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isScalarTower_mid'` `prod_embeddings_eq_finrank_pow`
`norm_eq_prod_roots` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `norm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Multiset.prod` `CommRing.toCommMonoid` `Polynomial.aroots` `instIsDomain` `Module.finrank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `IntermediateField.toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`instIsDomain` `IsScalarTower.left` `norm_eq_norm_adjoin` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots`
`norm_norm` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `norm`	—	`smulCommClass_self` `IsScalarTower.left` `norm_apply` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.det_restrictScalars`

Algebra.Norm.Transitivity

Definitions

Name	Category	Theorems
`auxMat` 📖	CompOp	8 math math: `comp_det_mul_pow`, `mul_auxMat_corner`, `mul_auxMat_blockTriangular`, `mul_auxMat_toSquareBlock_eq`, `auxMat_toSquareBlock_ne`, `auxMat_toSquareBlock_eq`, `auxMat_blockTriangular`, `det_mul_corner_pow`
`cornerAddX` 📖	CompOp	3 math math: `polyToMatrix_cornerAddX`, `eval_zero_comp_det`, `eval_zero_det_det`
`termMulAuxMatBlock` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`auxMat_blockTriangular` 📖	mathematical	—	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `Prop.partialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `auxMat`	—	`auxMat.eq_1` `Matrix.of_apply`
`auxMat_toSquareBlock_eq` 📖	mathematical	—	`Matrix.toSquareBlock` `auxMat` `Matrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Matrix.ext`
`auxMat_toSquareBlock_ne` 📖	mathematical	—	`Matrix.toSquareBlock` `auxMat` `Matrix` `Matrix.smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Matrix.ext` `mul_ite` `mul_one` `MulZeroClass.mul_zero`
`comp_det_mul_pow` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix.det` `instFintypeProd` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.comp` `Matrix.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card` `Subtype.fintype` `Matrix.toSquareBlock` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `auxMat`	—	`Matrix.det.congr_simp` `RingHom.mapMatrix_apply` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `Matrix.det_mul` `Matrix.BlockTriangular.det_fintype` `Matrix.BlockTriangular.comp` `Matrix.BlockTriangular.map` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `auxMat_blockTriangular` `Fintype.prod_Prop` `Matrix.comp_toSquareBlock` `Matrix.det_reindex_self` `Matrix.map_toSquareBlock` `auxMat_toSquareBlock_eq` `auxMat_toSquareBlock_ne` `Matrix.smul_one_eq_diagonal` `Matrix.diagonal_map` `map_zero` `Matrix.comp_diagonal` `Matrix.det_blockDiagonal` `Finset.prod_const` `Fintype.card_congr'` `Fintype.card_subtype_compl` `Fintype.card_unique` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `Finset.prod_congr` `Matrix.det_one` `Finset.prod_const_one` `mul_one` `mul_auxMat_blockTriangular` `mul_auxMat_toSquareBlock_eq` `pow_one`
`det_det_aux` 📖	mathematical	`Matrix.det` `DFunLike.coe` `RingHom` `Matrix` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `Subtype.fintype` `instFintypeProd` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.comp` `Matrix.map`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sub_mul` `comp_det_mul_pow` `Matrix.det_pow` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Matrix.det_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `det_mul_corner_pow` `sub_self`
`det_mul_corner_pow` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix.det` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Fintype.card` `Subtype.fintype` `Matrix.toSquareBlock` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `auxMat`	—	`Matrix.det_mul` `Matrix.BlockTriangular.det_fintype` `auxMat_blockTriangular` `Finset.prod_congr` `Fintype.univ_Prop` `Finset.prod_insert` `Matrix.det.congr_simp` `auxMat_toSquareBlock_ne` `Matrix.det_smul_of_tower` `IsScalarTower.right` `Algebra.to_smulCommClass` `Fintype.card_congr'` `Fintype.card_subtype_compl` `Fintype.card_unique` `Matrix.det_one` `mul_one` `Finset.prod_singleton` `auxMat_toSquareBlock_eq` `mul_auxMat_blockTriangular` `Fintype.prod_Prop` `mul_auxMat_toSquareBlock_eq` `pow_one` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton`
`eval_zero_comp_det` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix.det` `instFintypeProd` `Polynomial` `Polynomial.commRing` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.comp` `Matrix.map` `cornerAddX` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `RingHom.polyToMatrix`	—	`RingHom.map_det` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Matrix.det.congr_simp` `evalRingHom_mapMatrix_comp_compRingEquiv` `evalRingHom_mapMatrix_comp_polyToMatrix` `Matrix.ext` `Polynomial.eval_add` `Polynomial.eval_X` `Polynomial.eval_zero` `Polynomial.eval_C` `zero_add`
`eval_zero_det_det` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix.det` `Polynomial` `Polynomial.commRing` `DFunLike.coe` `RingHom` `Matrix` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `RingHom.polyToMatrix` `cornerAddX`	—	`Polynomial.coe_evalRingHom` `RingHom.map_det` `RingHom.comp_apply` `evalRingHom_mapMatrix_comp_polyToMatrix` `Matrix.ext` `Polynomial.eval_add` `Polynomial.eval_X` `Polynomial.eval_zero` `Polynomial.eval_C` `zero_add`
`mul_auxMat_blockTriangular` 📖	mathematical	—	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `Prop.partialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `auxMat`	—	`Finset.sum_congr` `mul_ite` `mul_neg` `MulZeroClass.mul_zero` `Finset.sum_ite` `Finset.filter_eq'` `Finset.mem_univ` `Finset.sum_singleton` `Finset.sum_ite_eq'` `Finset.mem_filter` `mul_comm` `neg_add_cancel`
`mul_auxMat_corner` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `auxMat`	—	`Finset.sum_congr` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'`
`mul_auxMat_toSquareBlock_eq` 📖	mathematical	—	`Matrix.toSquareBlock` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `auxMat` `Matrix.smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Matrix.ext` `mul_auxMat_corner` `Matrix.one_apply_eq` `mul_one`
`polyToMatrix_cornerAddX` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `RingHom.polyToMatrix` `cornerAddX` `Matrix.charmatrix` `Matrix.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Matrix.diagonal_apply_eq` `Polynomial.map_add` `Polynomial.map_X` `Polynomial.map_C` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `matPolyEquiv_symm_X` `matPolyEquiv_symm_C` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_neg_eq_add`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_restrictScalars` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `det` `restrictScalars` `IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Ring.toSemiring` `CommRing.toRing` `Algebra.norm`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `IsScalarTower.compatibleSMul` `det_eq_one_of_subsingleton` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `Module.nontrivial` `Module.Free.exists_basis` `Module.Basis.index_nonempty` `Algebra.norm_eq_matrix_det` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.coe_toRingHom` `RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `det_toMatrix` `Matrix.det_det` `Finite.instProd` `restrictScalars_toMatrix` `RingHom.coe_coe` `det_eq_one_of_not_module_finite` `Module.not_finite_of_infinite_basis` `Prod.infinite_of_right` `Algebra.norm_eq_one_of_not_module_finite` `Prod.infinite_of_left`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_det` 📖	mathematical	—	`det` `DFunLike.coe` `RingHom` `Matrix` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `nonAssocSemiring` `RingHom.instFunLike` `instFintypeProd` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `map`	—	`det.congr_simp` `det_isEmpty` `Fintype.card_eq_zero_iff` `Prod.isEmpty_left` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `det_one` `Fintype.card_pos_iff` `sub_eq_zero` `mem_nonZeroDivisors_iff_right` `pow_mem` `Submonoid.instSubmonoidClass` `Algebra.Norm.Transitivity.polyToMatrix_cornerAddX` `charpoly.eq_1` `Polynomial.Monic.mem_nonZeroDivisors` `charpoly_monic` `Algebra.Norm.Transitivity.det_det_aux` `Algebra.Norm.Transitivity.eval_zero_det_det` `Algebra.Norm.Transitivity.eval_zero_comp_det`

---

← Back to Index