StarRingHom

📁 Source: Mathlib/Algebra/Star/StarRingHom.lean

Statistics

Metric	Count
Definitions `NonUnitalStarRingHom`, `apply`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `instMonoid`, `instMonoidWithZero`, `instZero`, `toNonUnitalRingHom`, `NonUnitalStarRingHomClass`, `instCoeHeadNonUnitalStarRingHom`, `toNonUnitalStarRingHom`, `StarRingEquiv`, `apply`, `symm_apply`, `instEquivLike`, `instFunLike`, `instInhabited`, `ofBijective`, `ofStarRingHom`, `refl`, `aux`, `toRingEquiv`, `trans`, `StarRingEquivClass`, `instCoeHead`, `toStarRingEquiv`, `«term_→⋆ₙ+_»`, `«term_≃⋆+_»`	31
Theorems `coe_coe`, `coe_comp`, `coe_copy`, `coe_id`, `coe_mk`, `coe_one`, `coe_toNonUnitalRingHom`, `coe_zero`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `ext`, `ext_iff`, `id_comp`, `instNonUnitalRingHomClass`, `instNonUnitalStarRingHomClass`, `map_star'`, `mk_coe`, `one_apply`, `zero_apply`, `toStarHomClass`, `apply_symm_apply`, `coe_mk`, `coe_ofBijective`, `coe_refl`, `coe_trans`, `ext`, `ext_iff`, `instRingEquivClass`, `instStarRingEquivClass`, `invFun_eq_symm`, `leftInverse_symm`, `map_star'`, `mk_coe`, `ofBijective_apply`, `ofStarRingHom_apply`, `ofStarRingHom_symm_apply`, `refl_symm`, `rightInverse_symm`, `symm_apply_apply`, `symm_bijective`, `symm_mk`, `symm_symm`, `symm_trans_apply`, `toRingEquiv_eq_coe`, `trans_apply`, `instNonUnitalStarRingHomClass`, `instStarHomClass`, `map_star`, `toRingEquivClass`	51
Total	82

NonUnitalStarRingHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	5 math math: `comp_id`, `coe_comp`, `comp_assoc`, `comp_apply`, `id_comp`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`id` 📖	CompOp	3 math math: `comp_id`, `coe_id`, `id_comp`
`instFunLike` 📖	CompOp	16 math math: `coe_zero`, `CentroidHom.starCenterIsoCentroid_apply`, `one_apply`, `instNonUnitalStarRingHomClass`, `coe_mk`, `coe_id`, `instNonUnitalRingHomClass`, `coe_comp`, `zero_apply`, `map_le_map_of_map_star`, `coe_toNonUnitalRingHom`, `coe_one`, `coe_coe`, `comp_apply`, `CentroidHom.starCenterToCentroid_apply`, `ext_iff`
`instInhabited` 📖	CompOp	—
`instMonoid` 📖	CompOp	2 math math: `one_apply`, `coe_one`
`instMonoidWithZero` 📖	CompOp	—
`instZero` 📖	CompOp	2 math math: `coe_zero`, `zero_apply`
`toNonUnitalRingHom` 📖	CompOp	2 math math: `coe_toNonUnitalRingHom`, `map_star'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `NonUnitalStarRingHomClass.toNonUnitalStarRingHom`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`MulHom.toFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalRingHom.toMulHom` `Star.star`	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`coe_toNonUnitalRingHom` 📖	mathematical	—	`DFunLike.coe` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `toNonUnitalRingHom` `NonUnitalStarRingHom` `instFunLike`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `instZero` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instNonUnitalRingHomClass` 📖	mathematical	—	`NonUnitalRingHomClass` `NonUnitalStarRingHom` `instFunLike`	—	`MulHom.map_mul'` `NonUnitalRingHom.map_add'` `NonUnitalRingHom.map_zero'`
`instNonUnitalStarRingHomClass` 📖	mathematical	—	`NonUnitalStarRingHomClass` `NonUnitalStarRingHom` `instFunLike` `instNonUnitalRingHomClass`	—	`instNonUnitalRingHomClass` `map_star'`
`map_star'` 📖	mathematical	—	`MulHom.toFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalRingHom.toMulHom` `toNonUnitalRingHom` `Star.star`	—	—
`mk_coe` 📖	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddZero.toAdd` `NonUnitalRingHom.toMulHom` `Star.star`	—	—	`ext`
`one_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarRingHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—

NonUnitalStarRingHom.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

NonUnitalStarRingHomClass

Definitions

Name	Category	Theorems
`instCoeHeadNonUnitalStarRingHom` 📖	CompOp	—
`toNonUnitalStarRingHom` 📖	CompOp	1 math math: `NonUnitalStarRingHom.coe_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toStarHomClass` 📖	mathematical	—	`StarHomClass`	—	—

StarRingEquiv

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	4 math math: `toRingEquiv_eq_coe`, `invFun_eq_symm`, `instRingEquivClass`, `instStarRingEquivClass`
`instFunLike` 📖	CompOp	18 math math: `ofStarRingHom_apply`, `CentroidHom.starCenterIsoCentroid_symm_apply_coe`, `CentroidHom.starCenterIsoCentroid_apply`, `trans_apply`, `leftInverse_symm`, `rightInverse_symm`, `symm_apply_apply`, `apply_symm_apply`, `coe_refl`, `coe_ofBijective`, `invFun_eq_symm`, `ofBijective_apply`, `symm_trans_apply`, `StarAlgEquiv.coe_mk`, `coe_trans`, `coe_mk`, `ofStarRingHom_symm_apply`, `ext_iff`
`instInhabited` 📖	CompOp	—
`ofBijective` 📖	CompOp	2 math math: `coe_ofBijective`, `ofBijective_apply`
`ofStarRingHom` 📖	CompOp	2 math math: `ofStarRingHom_apply`, `ofStarRingHom_symm_apply`
`refl` 📖	CompOp	2 math math: `coe_refl`, `refl_symm`
`toRingEquiv` 📖	CompOp	6 math math: `StarAlgEquiv.restrictScalars_symm_apply`, `toRingEquiv_eq_coe`, `StarAlgEquiv.toRingEquiv_eq_coe`, `Unitary.toRingEquiv_conjStarAlgAut`, `map_star'`, `StarAlgEquiv.map_smul'`
`trans` 📖	CompOp	3 math math: `trans_apply`, `symm_trans_apply`, `coe_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `symm`	—	`RingEquiv.apply_symm_apply`
`coe_mk` 📖	mathematical	`Equiv.toFun` `RingEquiv.toEquiv` `Star.star`	`DFunLike.coe` `StarRingEquiv` `instFunLike` `RingEquiv` `EquivLike.toFunLike` `RingEquiv.instEquivLike`	—	—
`coe_ofBijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe`	`StarRingEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `instFunLike` `ofBijective`	—	—
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `refl`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `trans`	—	—
`ext` 📖	—	`DFunLike.coe` `StarRingEquiv` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike`	—	`ext`
`instRingEquivClass` 📖	mathematical	—	`RingEquivClass` `StarRingEquiv` `instEquivLike`	—	`RingEquiv.map_mul'` `RingEquiv.map_add'`
`instStarRingEquivClass` 📖	mathematical	—	`StarRingEquivClass` `StarRingEquiv` `instEquivLike`	—	`instRingEquivClass` `map_star'`
`invFun_eq_symm` 📖	mathematical	—	`EquivLike.inv` `StarRingEquiv` `instEquivLike` `DFunLike.coe` `instFunLike` `symm`	—	—
`leftInverse_symm` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `symm`	—	`Equiv.left_inv`
`map_star'` 📖	mathematical	—	`Equiv.toFun` `RingEquiv.toEquiv` `toRingEquiv` `Star.star`	—	—
`mk_coe` 📖	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `Equiv.toFun` `RingEquiv.toEquiv` `Star.star`	—	—	`ext`
`ofBijective_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe`	`StarRingEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `instFunLike` `ofBijective`	—	—
`ofStarRingHom_apply` 📖	mathematical	`DFunLike.coe`	`StarRingEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `instFunLike` `ofStarRingHom`	—	—
`ofStarRingHom_symm_apply` 📖	mathematical	`DFunLike.coe`	`StarRingEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `instFunLike` `symm` `ofStarRingHom`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`rightInverse_symm` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `symm`	—	`Equiv.right_inv`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `symm`	—	`RingEquiv.symm_apply_apply`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `StarRingEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_mk` 📖	mathematical	`Equiv.toFun` `RingEquiv.toEquiv` `Star.star`	`symm`	—	—
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_apply` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `symm` `trans`	—	—
`toRingEquiv_eq_coe` 📖	mathematical	—	`toRingEquiv` `RingEquivClass.toRingEquiv` `StarRingEquiv` `instEquivLike` `instRingEquivClass`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `instFunLike` `trans`	—	—

StarRingEquiv.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

StarRingEquiv.symm_mk

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	—

StarRingEquivClass

Definitions

Name	Category	Theorems
`instCoeHead` 📖	CompOp	—
`toStarRingEquiv` 📖	CompOp	2 math math: `StarAlgEquiv.toStarRingEquiv_symm`, `StarAlgEquiv.toStarRingEquiv_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonUnitalStarRingHomClass` 📖	mathematical	—	`NonUnitalStarRingHomClass` `EquivLike.toFunLike` `RingEquivClass.toNonUnitalRingHomClass`	—	`RingEquivClass.toNonUnitalRingHomClass` `instStarHomClass`
`instStarHomClass` 📖	mathematical	—	`StarHomClass` `EquivLike.toFunLike`	—	`map_star`
`map_star` 📖	mathematical	—	`DFunLike.coe` `EquivLike.toFunLike` `Star.star`	—	—
`toRingEquivClass` 📖	mathematical	—	`RingEquivClass`	—	—

(root)

Definitions

Name	Category	Theorems
`NonUnitalStarRingHom` 📖	CompData	16 math math: `NonUnitalStarRingHom.coe_zero`, `CentroidHom.starCenterIsoCentroid_apply`, `NonUnitalStarRingHom.one_apply`, `NonUnitalStarRingHom.instNonUnitalStarRingHomClass`, `NonUnitalStarRingHom.coe_mk`, `NonUnitalStarRingHom.coe_id`, `NonUnitalStarRingHom.instNonUnitalRingHomClass`, `NonUnitalStarRingHom.coe_comp`, `NonUnitalStarRingHom.zero_apply`, `NonUnitalStarRingHom.map_le_map_of_map_star`, `NonUnitalStarRingHom.coe_toNonUnitalRingHom`, `NonUnitalStarRingHom.coe_one`, `NonUnitalStarRingHom.coe_coe`, `NonUnitalStarRingHom.comp_apply`, `CentroidHom.starCenterToCentroid_apply`, `NonUnitalStarRingHom.ext_iff`
`NonUnitalStarRingHomClass` 📖	CompData	3 math math: `NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass`, `NonUnitalStarRingHom.instNonUnitalStarRingHomClass`, `StarRingEquivClass.instNonUnitalStarRingHomClass`
`StarRingEquiv` 📖	CompData	22 math math: `StarRingEquiv.ofStarRingHom_apply`, `CentroidHom.starCenterIsoCentroid_symm_apply_coe`, `CentroidHom.starCenterIsoCentroid_apply`, `StarRingEquiv.trans_apply`, `StarRingEquiv.toRingEquiv_eq_coe`, `StarRingEquiv.leftInverse_symm`, `StarRingEquiv.rightInverse_symm`, `StarRingEquiv.symm_apply_apply`, `StarRingEquiv.apply_symm_apply`, `StarRingEquiv.coe_refl`, `StarRingEquiv.coe_ofBijective`, `StarRingEquiv.invFun_eq_symm`, `StarRingEquiv.ofBijective_apply`, `StarRingEquiv.symm_trans_apply`, `StarRingEquiv.instRingEquivClass`, `StarRingEquiv.symm_bijective`, `StarRingEquiv.instStarRingEquivClass`, `StarAlgEquiv.coe_mk`, `StarRingEquiv.coe_trans`, `StarRingEquiv.coe_mk`, `StarRingEquiv.ofStarRingHom_symm_apply`, `StarRingEquiv.ext_iff`
`StarRingEquivClass` 📖	CompData	2 math math: `StarAlgEquiv.instStarRingEquivClass`, `StarRingEquiv.instStarRingEquivClass`
`«term_→⋆ₙ+*_»` 📖	CompOp	—
`«term_≃⋆+*_»` 📖	CompOp	—

---

← Back to Index