Composition

📁 Source: Mathlib/Data/Matrix/Composition.lean

Statistics

Metric	Count
Definitions `comp`, `compAddEquiv`, `compAlgEquiv`, `compLinearEquiv`, `compRingEquiv`	5
Theorems `compAddEquiv_apply`, `compAddEquiv_symm_apply`, `compAlgEquiv_apply`, `compAlgEquiv_symm_apply`, `compLinearEquiv_apply`, `compLinearEquiv_symm_apply`, `compRingEquiv_apply`, `compRingEquiv_symm_apply`, `comp_apply`, `comp_diagonal_diagonal`, `comp_map_map`, `comp_map_transpose`, `comp_one`, `comp_single_single`, `comp_symm_apply`, `comp_symm_diagonal`, `comp_symm_single`, `comp_symm_transpose`, `comp_transpose`, `instIsStablyFiniteRing`, `isUnit_comp_iff`, `isUnit_comp_symm_iff`	22
Total	27

Matrix

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	28 math math: `LinearMap.restrictScalars_toMatrix`, `comp_diagonal_diagonal`, `compAlgEquiv_apply`, `det_det`, `comp_single_single`, `Algebra.Norm.Transitivity.comp_det_mul_pow`, `comp_transpose`, `comp_toSquareBlock`, `comp_apply`, `compRingEquiv_symm_apply`, `BlockTriangular.comp`, `compLinearEquiv_symm_apply`, `Algebra.Norm.Transitivity.eval_zero_comp_det`, `comp_symm_diagonal`, `compAlgEquiv_symm_apply`, `isUnit_comp_iff`, `comp_map_map`, `comp_symm_transpose`, `comp_diagonal`, `compRingEquiv_apply`, `comp_symm_apply`, `comp_map_transpose`, `compLinearEquiv_apply`, `comp_symm_single`, `compAddEquiv_symm_apply`, `compAddEquiv_apply`, `isUnit_comp_symm_iff`, `comp_one`
`compAddEquiv` 📖	CompOp	2 math math: `compAddEquiv_symm_apply`, `compAddEquiv_apply`
`compAlgEquiv` 📖	CompOp	2 math math: `compAlgEquiv_apply`, `compAlgEquiv_symm_apply`
`compLinearEquiv` 📖	CompOp	2 math math: `compLinearEquiv_symm_apply`, `compLinearEquiv_apply`
`compRingEquiv` 📖	CompOp	3 math math: `compRingEquiv_symm_apply`, `evalRingHom_mapMatrix_comp_compRingEquiv`, `compRingEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `compAddEquiv` `Equiv` `Equiv.instEquivLike` `comp`	—	—
`compAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `compAddEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `comp`	—	—
`compAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `semiring` `instFintypeProd` `instAlgebra` `AlgEquiv.instFunLike` `compAlgEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp`	—	—
`compAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `semiring` `instFintypeProd` `instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `compAlgEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comp`	—	—
`compLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `compLinearEquiv` `Equiv` `Equiv.instEquivLike` `comp`	—	`RingHomInvPair.ids`
`compLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `compLinearEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `comp`	—	`RingHomInvPair.ids`
`compRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Matrix` `instMulOfFintypeOfAddCommMonoid` `addCommMonoid` `instFintypeProd` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `compRingEquiv` `Equiv` `Equiv.instEquivLike` `comp`	—	—
`compRingEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Matrix` `instMulOfFintypeOfAddCommMonoid` `instFintypeProd` `addCommMonoid` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `compRingEquiv` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `comp`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp`	—	—
`comp_diagonal_diagonal` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `diagonal` `zero`	—	`ext` `ne_or_eq` `diagonal_apply_ne` `zero_apply` `diagonal_apply_eq`
`comp_map_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `map`	—	—
`comp_map_transpose` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `map` `transpose`	—	—
`comp_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `one` `zero`	—	`ext` `one_apply_ne` `one_apply_eq`
`comp_single_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `single` `zero`	—	`ext` `ne_or_eq` `single_apply_of_row_ne` `zero_apply` `single_apply_of_col_ne` `single_apply_same`
`comp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comp`	—	—
`comp_symm_diagonal` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comp` `diagonal` `zero`	—	`Equiv.symm_apply_eq` `comp_diagonal_diagonal`
`comp_symm_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comp` `single` `zero`	—	`Equiv.symm_apply_eq` `comp_single_single`
`comp_symm_transpose` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comp` `transpose` `map`	—	—
`comp_transpose` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `transpose` `map`	—	—
`instIsStablyFiniteRing` 📖	mathematical	—	`IsStablyFiniteRing` `Matrix` `instMulOneOfFintypeOfDecidableEqOfAddCommMonoid` `addCommMonoid`	—	`IsDedekindFiniteMonoid.of_injective` `MonoidHom.instMonoidHomClass` `comp_one` `RingEquiv.map_mul` `RingEquiv.injective` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing`
`isUnit_comp_iff` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instFintypeProd` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp`	—	`isUnit_map_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `isLocalHom_equiv` `RingEquivClass.toMulEquivClass` `AlgEquivClass.toRingEquivClass`
`isUnit_comp_symm_iff` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comp` `instFintypeProd`	—	`isUnit_map_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `isLocalHom_equiv` `RingEquivClass.toMulEquivClass` `AlgEquivClass.toRingEquivClass`

---

← Back to Index