Unitization

📁 Source: Mathlib/Algebra/Algebra/Unitization.lean

Statistics

Metric	Count
Definitions `toAlgHom`, `addEquiv`, `delabMk`, `equiv`, `fstHom`, `inl`, `inlRingHom`, `inr`, `inrHom`, `inrNonUnitalAlgHom`, `inrNonUnitalStarAlgHom`, `inrRangeEquiv`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddCommSemigroup`, `instAddGroup`, `instAddMonoid`, `instAddSemigroup`, `instAddZeroClass`, `instAlgebra`, `instCoeOfZero`, `instCommMonoid`, `instCommRing`, `instCommSemiring`, `instDistribMulAction`, `instInhabited`, `instModule`, `instMonoid`, `instMul`, `instMulAction`, `instMulOneClass`, `instNeg`, `instNonAssocRing`, `instNonAssocSemiring`, `instOne`, `instRing`, `instSMul`, `instSemiring`, `instStar`, `instStarAddMonoid`, `instStarRing`, `instSub`, `instZero`, `linearEquiv`, `sndHom`, `starLift`, `starMap`, `toProd`	49
Theorems `inr`, `of_inr`, `of_inr`, `inr`, `of_inr`, `toAlgHom_apply`, `toAlgHom_zero`, `inr`, `addEquiv_apply`, `addEquiv_symm_apply`, `algHom_ext`, `algHom_ext'`, `algHom_ext''`, `algHom_ext'_iff`, `algebraMap_eq_inl`, `algebraMap_eq_inlRingHom`, `algebraMap_eq_inlRingHom_comp`, `algebraMap_eq_inl_comp`, `equiv_apply`, `equiv_symm_apply`, `ext`, `ext_iff`, `fstHom_apply`, `fst_add`, `fst_inl`, `fst_inr`, `fst_mul`, `fst_neg`, `fst_one`, `fst_smul`, `fst_star`, `fst_zero`, `ind`, `inlRingHom_apply`, `inl_add`, `inl_fst_add_inr_snd_eq`, `inl_inj`, `inl_injective`, `inl_mul`, `inl_mul_inl`, `inl_mul_inr`, `inl_neg`, `inl_one`, `inl_smul`, `inl_star`, `inl_sub`, `inl_zero`, `inrHom_apply`, `inrNonUnitalAlgHom_apply`, `inrNonUnitalAlgHom_toFun`, `inrNonUnitalStarAlgHom_apply`, `inrRangeEquiv_apply_coe_fst`, `inrRangeEquiv_apply_coe_snd`, `inrRangeEquiv_symm_apply`, `inr_add`, `inr_inj`, `inr_injective`, `inr_mul`, `inr_mul_inl`, `inr_neg`, `inr_smul`, `inr_star`, `inr_sub`, `inr_zero`, `instCanLift`, `instIsCentralScalar`, `instIsScalarTower`, `instIsStarNormal`, `instNontrivialLeft`, `instNontrivialRight`, `instSMulCommClass`, `instStarModule`, `isIdempotentElem_inr_iff`, `isSelfAdjoint_inr`, `isStarNormal_inr`, `isStarProjection_inr_iff`, `lift_apply`, `lift_apply_apply`, `lift_symm_apply`, `lift_symm_apply_apply`, `linearEquiv_apply`, `linearEquiv_symm_apply`, `linearMap_ext`, `linearMap_ext_iff`, `mk_bijective`, `mk_injective`, `mk_surjective`, `mk_toProd`, `sndHom_apply`, `snd_add`, `snd_inl`, `snd_inr`, `snd_mul`, `snd_neg`, `snd_one`, `snd_smul`, `snd_star`, `snd_zero`, `starAlgHom_ext`, `starAlgHom_ext_iff`, `starLift_apply`, `starLift_apply_apply`, `starLift_symm_apply`, `starLift_symm_apply_apply`, `starMap_apply`, `starMap_comp`, `starMap_id`, `starMap_injective`, `starMap_inl`, `starMap_inr`, `starMap_surjective`, `toAddEquiv_linearEquiv`, `toEquiv_addEquiv`, `toProd_add`, `toProd_bijective`, `toProd_inj_iff`, `toProd_injective`, `toProd_mk`, `toProd_neg`, `toProd_smul`, `toProd_surjective`, `toProd_zero`	122
Total	171

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inr` 📖	mathematical	`IsSelfAdjoint`	`IsSelfAdjoint` `Unitization` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Unitization.isSelfAdjoint_inr`
`of_inr` 📖	mathematical	`IsSelfAdjoint` `Unitization` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`IsSelfAdjoint`	—	`Unitization.isSelfAdjoint_inr`

IsStarNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_inr` 📖	mathematical	—	`IsStarNormal`	—	`Unitization.isStarNormal_inr`

IsStarProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inr` 📖	mathematical	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`IsStarProjection` `Unitization` `Unitization.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Unitization.isStarProjection_inr_iff`
`of_inr` 📖	mathematical	`IsStarProjection` `Unitization` `Unitization.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`IsStarProjection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`Unitization.isStarProjection_inr_iff`

NonUnitalAlgHom

Definitions

Name	Category	Theorems
`toAlgHom` 📖	CompOp	4 math math: `toAlgHom_zero`, `Unitization.starLift_apply`, `toAlgHom_apply`, `Unitization.lift_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Unitization` `Unitization.instSemiring` `Unitization.instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AlgHom.funLike` `toAlgHom` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom` `RingHom.instFunLike` `algebraMap` `Unitization.toProd` `NonUnitalAlgHom` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Algebra.toModule` `instFunLike_1`	—	`IsScalarTower.left`
`toAlgHom_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Unitization` `Unitization.instSemiring` `CommSemiring.toSemiring` `Unitization.instAlgebra` `Algebra.id` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AlgHom.funLike` `toAlgHom` `NonUnitalAlgHom` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instZero` `Unitization.toProd`	—	`IsScalarTower.left` `add_zero`

Unitization

Definitions

Name	Category	Theorems
`addEquiv` 📖	CompOp	9 math math: `toEquiv_addEquiv`, `cobounded_eq_aux`, `toAddEquiv_linearEquiv`, `addEquiv_symm_apply`, `isUniformEmbedding_addEquiv`, `antilipschitzWith_addEquiv`, `uniformity_eq_aux`, `lipschitzWith_addEquiv`, `addEquiv_apply`
`delabMk` 📖	CompOp	—
`equiv` 📖	CompOp	3 math math: `toEquiv_addEquiv`, `equiv_symm_apply`, `equiv_apply`
`fstHom` 📖	CompOp	1 math math: `fstHom_apply`
`inl` 📖	CompOp	21 math math: `inl_mul_inr`, `inl_injective`, `fst_inl`, `inl_one`, `inl_mul`, `inl_zero`, `inl_star`, `linearMap_ext_iff`, `starMap_inl`, `inl_mul_inl`, `algebraMap_eq_inl`, `inr_mul_inl`, `inl_inj`, `inl_neg`, `inl_add`, `inl_sub`, `snd_inl`, `inl_smul`, `inl_fst_add_inr_snd_eq`, `inlRingHom_apply`, `algebraMap_eq_inl_comp`
`inlRingHom` 📖	CompOp	3 math math: `algebraMap_eq_inlRingHom_comp`, `algebraMap_eq_inlRingHom`, `inlRingHom_apply`
`inr` 📖	CompOp	64 math math: `CStarAlgebra.preimage_inr_Icc_zero_one`, `inr_neg`, `isometry_inr`, `inrNonUnitalAlgHom_toFun`, `inr_inj`, `CStarAlgebra.inr_mem_Icc_iff_norm_le`, `quasispectrumRestricts_iff_spectrumRestricts_inr'`, `real_cfcₙ_eq_cfc_inr`, `fst_inr`, `inr_sub`, `inl_mul_inr`, `isIdempotentElem_inr_iff`, `isQuasiregular_inr_iff`, `starLift_symm_apply_apply`, `sqrt_inr`, `inr_star`, `inr_le_iff`, `dist_inr`, `snd_inr`, `lift_symm_apply_apply`, `quasispectrum_inr_eq`, `zero_mem_spectrum_inr`, `cfcₙAux_id`, `IsSelfAdjoint.inr`, `inr_mul`, `instCanLift`, `isStarProjection_inr_iff`, `inr_smul`, `inrNonUnitalStarAlgHom_apply`, `linearMap_ext_iff`, `starMap_inr`, `val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `isSelfAdjoint_inr`, `val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `inr_injective`, `inrHom_apply`, `mem_spectrum_inr_of_not_isUnit`, `WithLp.unitization_nnnorm_inr`, `inr_add`, `IsStarProjection.inr`, `inr_mul_inl`, `nnreal_cfcₙ_eq_cfc_inr`, `IsIdempotentElem.inr`, `quasispectrumRestricts_iff_spectrumRestricts_inr`, `starMap_apply`, `instIsStarNormal`, `inr_zero`, `quasispectrum_eq_spectrum_inr'`, `complex_cfcₙ_eq_cfc_inr`, `LE.le.inr`, `inrNonUnitalAlgHom_apply`, `nndist_inr`, `isQuasiregular_iff_isUnit'`, `CStarAlgebra.inr_mem_Icc_iff_nnnorm_le`, `quasispectrum_eq_spectrum_inr`, `WithLp.unitization_norm_inr`, `inl_fst_add_inr_snd_eq`, `WithLp.unitization_isometry_inr`, `norm_inr`, `inr_nonneg_iff`, `continuous_inr`, `isStarNormal_inr`, `nnnorm_inr`, `cfcₙ_eq_cfc_inr`
`inrHom` 📖	CompOp	1 math math: `inrHom_apply`
`inrNonUnitalAlgHom` 📖	CompOp	4 math math: `inrNonUnitalAlgHom_toFun`, `algHom_ext'_iff`, `lift_symm_apply`, `inrNonUnitalAlgHom_apply`
`inrNonUnitalStarAlgHom` 📖	CompOp	9 math math: `starAlgHom_ext_iff`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `inrNonUnitalStarAlgHom_apply`, `inrRangeEquiv_apply_coe_snd`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `inrRangeEquiv_apply_coe_fst`, `cfcₙAux_mem_range_inr`, `starLift_symm_apply`, `inrRangeEquiv_symm_apply`
`inrRangeEquiv` 📖	CompOp	3 math math: `inrRangeEquiv_apply_coe_snd`, `inrRangeEquiv_apply_coe_fst`, `inrRangeEquiv_symm_apply`
`instAdd` 📖	CompOp	18 math math: `toEquiv_addEquiv`, `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `toProd_add`, `cobounded_eq_aux`, `fst_add`, `val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `inr_add`, `addEquiv_symm_apply`, `isUniformEmbedding_addEquiv`, `isQuasiregular_iff_isUnit'`, `snd_add`, `antilipschitzWith_addEquiv`, `uniformity_eq_aux`, `inl_add`, `lipschitzWith_addEquiv`, `addEquiv_apply`, `inl_fst_add_inr_snd_eq`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	6 math math: `linearEquiv_symm_apply`, `linearMap_ext_iff`, `toAddEquiv_linearEquiv`, `sndHom_apply`, `inrHom_apply`, `linearEquiv_apply`
`instAddCommSemigroup` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAddSemigroup` 📖	CompOp	—
`instAddZeroClass` 📖	CompOp	—
`instAlgebra` 📖	CompOp	61 math math: `quasispectrumRestricts_iff_spectrumRestricts_inr'`, `real_cfcₙ_eq_cfc_inr`, `splitMul_apply`, `algHom_ext'_iff`, `starAlgHom_ext_iff`, `starLift_symm_apply_apply`, `starLift_apply_apply`, `sqrt_inr`, `nnnorm_def`, `WithLp.unitization_algebraMap`, `NonUnitalSubalgebra.unitization_injective`, `lift_symm_apply_apply`, `NonUnitalStarSubalgebra.unitization_range`, `NonUnitalSubalgebra.unitization_range`, `NonUnitalSubsemiring.unitization_apply`, `NonUnitalSubring.unitization_apply`, `zero_mem_spectrum_inr`, `splitMul_injective_of_clm_mul_injective`, `starMap_injective`, `NonUnitalAlgHom.toAlgHom_zero`, `starMap_id`, `starLift_range`, `starMap_inl`, `starMap_inr`, `algebraMap_eq_inl`, `NonUnitalStarSubalgebra.unitization_injective`, `NonUnitalStarSubalgebra.unitization_apply`, `starMap_surjective`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe`, `mem_spectrum_inr_of_not_isUnit`, `lift_range`, `algebraMap_eq_inlRingHom_comp`, `NonUnitalSubalgebra.unitization_apply`, `lift_symm_apply`, `norm_def`, `WithLp.unitizationAlgEquiv_symm_apply_ofLp`, `spec_cfcₙAux`, `nnreal_cfcₙ_eq_cfc_inr`, `starLift_apply`, `starMap_comp`, `quasispectrumRestricts_iff_spectrumRestricts_inr`, `fstHom_apply`, `starMap_apply`, `NonUnitalSubring.unitization_range`, `NonUnitalAlgHom.toAlgHom_apply`, `quasispectrum_eq_spectrum_inr'`, `NonUnitalSubsemiring.unitization_range`, `complex_cfcₙ_eq_cfc_inr`, `lift_range_le`, `norm_splitMul_snd_sq`, `splitMul_injective`, `starLift_range_le`, `lift_apply_apply`, `starLift_symm_apply`, `WithLp.unitizationAlgEquiv_apply`, `algebraMap_eq_inlRingHom`, `quasispectrum_eq_spectrum_inr`, `lift_apply`, `algebraMap_eq_inl_comp`, `cfcₙ_eq_cfc_inr`
`instCoeOfZero` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	15 math math: `inrNonUnitalAlgHom_toFun`, `isClosedEmbedding_cfcₙAux`, `starAlgHom_ext_iff`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `cfcₙAux_id`, `inrNonUnitalStarAlgHom_apply`, `inrRangeEquiv_apply_coe_snd`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `inrRangeEquiv_apply_coe_fst`, `cfcₙAux_injective`, `spec_cfcₙAux`, `cfcₙAux_mem_range_inr`, `inrNonUnitalAlgHom_apply`, `continuous_cfcₙAux`, `inrRangeEquiv_symm_apply`
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	12 math math: `sqrt_inr`, `linearEquiv_symm_apply`, `quasispectrum_inr_eq`, `linearMap_ext_iff`, `toAddEquiv_linearEquiv`, `sndHom_apply`, `inrRangeEquiv_apply_coe_snd`, `inrHom_apply`, `inrRangeEquiv_apply_coe_fst`, `cfcₙAux_mem_range_inr`, `linearEquiv_apply`, `inrRangeEquiv_symm_apply`
`instMonoid` 📖	CompOp	8 math math: `val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `val_inv_unitsFstOne_mulEquiv_quasiregular_apply`, `isQuasiregular_iff_isUnit'`, `val_unitsFstOne_mulEquiv_quasiregular_apply`, `unitsFstOne_val_val_fst`, `mem_unitsFstOne`, `unitsFstOne_val_inv_val_fst`
`instMul` 📖	CompOp	17 math math: `inl_mul_inr`, `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `isIdempotentElem_inr_iff`, `inl_mul`, `snd_mul`, `fst_mul`, `inr_mul`, `isStarProjection_inr_iff`, `inl_mul_inl`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `IsStarProjection.inr`, `inr_mul_inl`, `IsIdempotentElem.inr`, `instIsStarNormal`, `norm_splitMul_snd_sq`, `WithLp.unitization_mul`, `isStarNormal_inr`
`instMulAction` 📖	CompOp	—
`instMulOneClass` 📖	CompOp	—
`instNeg` 📖	CompOp	5 math math: `toProd_neg`, `inr_neg`, `snd_neg`, `inl_neg`, `fst_neg`
`instNonAssocRing` 📖	CompOp	6 math math: `isClosedEmbedding_cfcₙAux`, `cfcₙAux_id`, `cfcₙAux_injective`, `spec_cfcₙAux`, `cfcₙAux_mem_range_inr`, `continuous_cfcₙAux`
`instNonAssocSemiring` 📖	CompOp	12 math math: `inrNonUnitalAlgHom_toFun`, `starAlgHom_ext_iff`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `inrNonUnitalStarAlgHom_apply`, `inrRangeEquiv_apply_coe_snd`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `inrRangeEquiv_apply_coe_fst`, `algebraMap_eq_inlRingHom_comp`, `cfcₙAux_mem_range_inr`, `inrNonUnitalAlgHom_apply`, `inrRangeEquiv_symm_apply`, `inlRingHom_apply`
`instOne` 📖	CompOp	10 math math: `CStarAlgebra.preimage_inr_Icc_zero_one`, `CStarAlgebra.inr_mem_Icc_iff_norm_le`, `inl_one`, `val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe`, `fst_one`, `snd_one`, `instNormOneClass`, `isQuasiregular_iff_isUnit'`, `CStarAlgebra.inr_mem_Icc_iff_nnnorm_le`
`instRing` 📖	CompOp	13 math math: `quasispectrumRestricts_iff_spectrumRestricts_inr'`, `real_cfcₙ_eq_cfc_inr`, `quasispectrum_inr_eq`, `zero_mem_spectrum_inr`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `mem_spectrum_inr_of_not_isUnit`, `spec_cfcₙAux`, `nnreal_cfcₙ_eq_cfc_inr`, `quasispectrumRestricts_iff_spectrumRestricts_inr`, `quasispectrum_eq_spectrum_inr'`, `complex_cfcₙ_eq_cfc_inr`, `quasispectrum_eq_spectrum_inr`, `cfcₙ_eq_cfc_inr`
`instSMul` 📖	CompOp	10 math math: `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `instSMulCommClass`, `inr_smul`, `instIsCentralScalar`, `instStarModule`, `instIsScalarTower`, `fst_smul`, `inl_smul`, `toProd_smul`, `snd_smul`
`instSemiring` 📖	CompOp	54 math math: `splitMul_apply`, `algHom_ext'_iff`, `starAlgHom_ext_iff`, `isQuasiregular_inr_iff`, `starLift_symm_apply_apply`, `starLift_apply_apply`, `sqrt_inr`, `nnnorm_def`, `instStarOrderedRing`, `WithLp.unitization_algebraMap`, `NonUnitalSubalgebra.unitization_injective`, `lift_symm_apply_apply`, `NonUnitalStarSubalgebra.unitization_range`, `NonUnitalSubalgebra.unitization_range`, `NonUnitalSubsemiring.unitization_apply`, `NonUnitalSubring.unitization_apply`, `splitMul_injective_of_clm_mul_injective`, `starMap_injective`, `NonUnitalAlgHom.toAlgHom_zero`, `starMap_id`, `starLift_range`, `starMap_inl`, `starMap_inr`, `algebraMap_eq_inl`, `inrRangeEquiv_apply_coe_snd`, `NonUnitalStarSubalgebra.unitization_injective`, `NonUnitalStarSubalgebra.unitization_apply`, `starMap_surjective`, `NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe`, `inrRangeEquiv_apply_coe_fst`, `lift_range`, `algebraMap_eq_inlRingHom_comp`, `NonUnitalSubalgebra.unitization_apply`, `lift_symm_apply`, `norm_def`, `WithLp.unitizationAlgEquiv_symm_apply_ofLp`, `starLift_apply`, `starMap_comp`, `fstHom_apply`, `starMap_apply`, `NonUnitalSubring.unitization_range`, `NonUnitalAlgHom.toAlgHom_apply`, `NonUnitalSubsemiring.unitization_range`, `lift_range_le`, `norm_splitMul_snd_sq`, `splitMul_injective`, `starLift_range_le`, `lift_apply_apply`, `starLift_symm_apply`, `WithLp.unitizationAlgEquiv_apply`, `algebraMap_eq_inlRingHom`, `lift_apply`, `inrRangeEquiv_symm_apply`, `algebraMap_eq_inl_comp`
`instStar` 📖	CompOp	41 math math: `isClosedEmbedding_cfcₙAux`, `starAlgHom_ext_iff`, `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `starLift_symm_apply_apply`, `starLift_apply_apply`, `inr_star`, `inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux`, `cfcₙAux_id`, `starMap_injective`, `IsSelfAdjoint.inr`, `starMap_id`, `isStarProjection_inr_iff`, `starLift_range`, `inl_star`, `inrNonUnitalStarAlgHom_apply`, `starMap_inl`, `starMap_inr`, `inrRangeEquiv_apply_coe_snd`, `isSelfAdjoint_inr`, `NonUnitalStarSubalgebra.unitization_injective`, `NonUnitalStarSubalgebra.unitization_apply`, `starMap_surjective`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `inrRangeEquiv_apply_coe_fst`, `cfcₙAux_injective`, `IsStarProjection.inr`, `spec_cfcₙAux`, `starLift_apply`, `starMap_comp`, `starMap_apply`, `instIsStarNormal`, `cfcₙAux_mem_range_inr`, `snd_star`, `instStarModule`, `continuous_cfcₙAux`, `norm_splitMul_snd_sq`, `starLift_range_le`, `starLift_symm_apply`, `inrRangeEquiv_symm_apply`, `fst_star`, `isStarNormal_inr`
`instStarAddMonoid` 📖	CompOp	—
`instStarRing` 📖	CompOp	11 math math: `real_cfcₙ_eq_cfc_inr`, `sqrt_inr`, `instStarOrderedRing`, `NonUnitalStarSubalgebra.unitization_range`, `starLift_range`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `nnreal_cfcₙ_eq_cfc_inr`, `instCStarRing`, `complex_cfcₙ_eq_cfc_inr`, `starLift_range_le`, `cfcₙ_eq_cfc_inr`
`instSub` 📖	CompOp	2 math math: `inr_sub`, `inl_sub`
`instZero` 📖	CompOp	10 math math: `CStarAlgebra.preimage_inr_Icc_zero_one`, `CStarAlgebra.inr_mem_Icc_iff_norm_le`, `fst_zero`, `inl_zero`, `toProd_zero`, `inr_zero`, `snd_zero`, `LE.le.inr`, `CStarAlgebra.inr_mem_Icc_iff_nnnorm_le`, `inr_nonneg_iff`
`linearEquiv` 📖	CompOp	3 math math: `linearEquiv_symm_apply`, `toAddEquiv_linearEquiv`, `linearEquiv_apply`
`sndHom` 📖	CompOp	1 math math: `sndHom_apply`
`starLift` 📖	CompOp	6 math math: `starLift_symm_apply_apply`, `starLift_apply_apply`, `starLift_range`, `starLift_apply`, `starLift_range_le`, `starLift_symm_apply`
`starMap` 📖	CompOp	7 math math: `starMap_injective`, `starMap_id`, `starMap_inl`, `starMap_inr`, `starMap_surjective`, `starMap_comp`, `starMap_apply`
`toProd` 📖	CompOp	64 math math: `toProd_neg`, `fst_inr`, `splitMul_apply`, `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `toProd_surjective`, `fst_inl`, `starLift_apply_apply`, `uniformContinuous_fst`, `fst_zero`, `snd_inr`, `snd_mul`, `fst_mul`, `NonUnitalSubsemiring.unitization_apply`, `toProd_add`, `NonUnitalSubring.unitization_apply`, `NonUnitalAlgHom.toAlgHom_zero`, `instCanLift`, `fst_add`, `toProd_injective`, `sndHom_apply`, `inrRangeEquiv_apply_coe_snd`, `NonUnitalStarSubalgebra.unitization_apply`, `continuous_snd`, `norm_eq_sup`, `NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe`, `toProd_zero`, `inrRangeEquiv_apply_coe_fst`, `val_inv_unitsFstOne_mulEquiv_quasiregular_apply`, `NonUnitalSubalgebra.unitization_apply`, `ext_iff`, `WithLp.unitization_norm_def`, `uniformContinuous_snd`, `fst_one`, `mk_toProd`, `fstHom_apply`, `starMap_apply`, `snd_one`, `NonUnitalAlgHom.toAlgHom_apply`, `nnnorm_eq_sup`, `snd_zero`, `snd_star`, `snd_add`, `linearEquiv_apply`, `toProd_mk`, `snd_neg`, `lift_apply_apply`, `fst_smul`, `toProd_bijective`, `toProd_inj_iff`, `snd_inl`, `val_unitsFstOne_mulEquiv_quasiregular_apply`, `addEquiv_apply`, `continuous_fst`, `unitsFstOne_val_val_fst`, `WithLp.unitization_nnnorm_def`, `inrRangeEquiv_symm_apply`, `fst_star`, `inl_fst_add_inr_snd_eq`, `toProd_smul`, `equiv_apply`, `mem_unitsFstOne`, `fst_neg`, `unitsFstOne_val_inv_val_fst`, `snd_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Unitization` `instAdd` `Prod.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquiv` `toProd`	—	—
`addEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Unitization` `Prod.instAdd` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquiv`	—	—
`algHom_ext` 📖	—	`DFunLike.coe` `Unitization` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	—	`IsScalarTower.left` `DFunLike.ext` `ind` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass`
`algHom_ext'` 📖	—	`NonUnitalAlgHom.comp` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Unitization` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AlgHom.toNonUnitalAlgHom` `inrNonUnitalAlgHom` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	—	`IsScalarTower.left` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `algHom_ext''` `AlgHom.algHomClass` `NonUnitalAlgHom.congr_fun`
`algHom_ext''` 📖	—	`DFunLike.coe` `Unitization` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`IsScalarTower.left` `algHom_ext` `AlgHomClass.commutes`
`algHom_ext'_iff` 📖	mathematical	—	`NonUnitalAlgHom.comp` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Unitization` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AlgHom.toNonUnitalAlgHom` `inrNonUnitalAlgHom` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	`IsScalarTower.left` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `algHom_ext'`
`algebraMap_eq_inl` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Unitization` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `inl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsScalarTower.left`
`algebraMap_eq_inlRingHom` 📖	mathematical	—	`algebraMap` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `inlRingHom`	—	`IsScalarTower.left`
`algebraMap_eq_inlRingHom_comp` 📖	mathematical	—	`algebraMap` `Unitization` `instSemiring` `instAlgebra` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `inlRingHom`	—	—
`algebraMap_eq_inl_comp` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Unitization` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `inl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	—
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Unitization` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `toProd`	—	—
`equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Unitization` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv`	—	—
`ext` 📖	—	`toProd`	—	—	—
`ext_iff` 📖	mathematical	—	`toProd`	—	`ext`
`fstHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Unitization` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AlgHom.funLike` `fstHom` `toProd`	—	`IsScalarTower.left`
`fst_add` 📖	mathematical	—	`toProd` `Unitization` `instAdd`	—	—
`fst_inl` 📖	mathematical	—	`toProd` `inl`	—	—
`fst_inr` 📖	mathematical	—	`toProd` `inr`	—	—
`fst_mul` 📖	mathematical	—	`toProd` `Unitization` `instMul`	—	—
`fst_neg` 📖	mathematical	—	`toProd` `Unitization` `instNeg`	—	—
`fst_one` 📖	mathematical	—	`toProd` `Unitization` `instOne`	—	—
`fst_smul` 📖	mathematical	—	`toProd` `Unitization` `instSMul`	—	—
`fst_star` 📖	mathematical	—	`toProd` `Star.star` `Unitization` `instStar`	—	—
`fst_zero` 📖	mathematical	—	`toProd` `Unitization` `instZero`	—	—
`ind` 📖	—	`Unitization` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `inl` `AddZero.toZero` `inr`	—	—	`inl_fst_add_inr_snd_eq`
`inlRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Unitization` `Semiring.toNonAssocSemiring` `instNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `RingHom.instFunLike` `inlRingHom` `inl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`inl_add` 📖	mathematical	—	`inl` `AddZero.toZero` `AddZeroClass.toAddZero` `Unitization` `instAdd` `AddZero.toAdd`	—	`ext` `add_zero`
`inl_fst_add_inr_snd_eq` 📖	mathematical	—	`Unitization` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `inl` `AddZero.toZero` `toProd` `inr`	—	`ext` `add_zero` `zero_add`
`inl_inj` 📖	mathematical	—	`inl`	—	`inl_injective`
`inl_injective` 📖	mathematical	—	`Unitization` `inl`	—	`fst_inl`
`inl_mul` 📖	mathematical	—	`inl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Unitization` `instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul`	—	`ext` `smul_zero` `add_zero` `MulZeroClass.mul_zero`
`inl_mul_inl` 📖	mathematical	—	`Unitization` `instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `inl`	—	`inl_mul`
`inl_mul_inr` 📖	mathematical	—	`Unitization` `instMul` `MulZeroClass.toMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `inl` `inr`	—	`ext` `MulZeroClass.mul_zero` `smul_zero` `add_zero` `MulZeroClass.zero_mul` `inr_smul`
`inl_neg` 📖	mathematical	—	`inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Unitization` `instNeg` `NegZeroClass.toNeg`	—	`ext` `neg_zero`
`inl_one` 📖	mathematical	—	`inl` `Unitization` `instOne`	—	—
`inl_smul` 📖	mathematical	—	`inl` `Unitization` `instSMul` `SMulZeroClass.toSMul`	—	`ext` `smul_zero`
`inl_star` 📖	mathematical	—	`inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Star.star` `Unitization` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar`	—	`ext` `star_zero`
`inl_sub` 📖	mathematical	—	`inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Unitization` `instSub`	—	`ext` `sub_zero`
`inl_zero` 📖	mathematical	—	`inl` `Unitization` `instZero`	—	—
`inrHom_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Unitization` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `inrHom` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`inrNonUnitalAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Unitization` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `instDistribMulAction` `AddCommMonoid.toAddMonoid` `Semiring.toModule` `NonUnitalAlgHom.instFunLike` `inrNonUnitalAlgHom` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`inrNonUnitalAlgHom_toFun` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Unitization` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `instDistribMulAction` `AddCommMonoid.toAddMonoid` `Semiring.toModule` `NonUnitalAlgHom.instFunLike` `inrNonUnitalAlgHom` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`inrNonUnitalStarAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `Unitization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `instDistribMulAction` `AddCommMonoid.toAddMonoid` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `NonUnitalStarAlgHom.instFunLike` `inrNonUnitalStarAlgHom` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`inrRangeEquiv_apply_coe_fst` 📖	mathematical	—	`toProd` `Unitization` `NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instSemiring` `instModule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgHom.range` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instNonAssocSemiring` `instDistribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalStarAlgHom.instFunLike` `inrNonUnitalStarAlgHom` `DFunLike.coe` `StarAlgEquiv` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalStarSubalgebra.toNonUnitalSemiring` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NonUnitalStarSubalgebra.instModule` `StarMemClass.instStar` `NonUnitalStarSubalgebra.instStarMemClass` `StarAlgEquiv.instFunLike` `inrRangeEquiv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `NonUnitalStarSubalgebra.instStarMemClass`
`inrRangeEquiv_apply_coe_snd` 📖	mathematical	—	`toProd` `Unitization` `NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instSemiring` `instModule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgHom.range` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instNonAssocSemiring` `instDistribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalStarAlgHom.instFunLike` `inrNonUnitalStarAlgHom` `DFunLike.coe` `StarAlgEquiv` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalStarSubalgebra.toNonUnitalSemiring` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NonUnitalStarSubalgebra.instModule` `StarMemClass.instStar` `NonUnitalStarSubalgebra.instStarMemClass` `StarAlgEquiv.instFunLike` `inrRangeEquiv`	—	`NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `NonUnitalStarSubalgebra.instStarMemClass`
`inrRangeEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Unitization` `NonUnitalStarSubalgebra` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgHom.range` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instDistribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalStarAlgHom.instFunLike` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `inrNonUnitalStarAlgHom` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalStarSubalgebra.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `instSemiring` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NonUnitalStarSubalgebra.instModule` `StarMemClass.instStar` `NonUnitalStarSubalgebra.instStarMemClass` `StarAlgEquiv.instFunLike` `StarAlgEquiv.symm` `inrRangeEquiv` `toProd`	—	`NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `NonUnitalStarSubalgebra.instStarMemClass`
`inr_add` 📖	mathematical	—	`inr` `AddZero.toZero` `AddZeroClass.toAddZero` `Unitization` `instAdd` `AddZero.toAdd`	—	`ext` `add_zero`
`inr_inj` 📖	mathematical	—	`inr`	—	`inr_injective`
`inr_injective` 📖	mathematical	—	`Unitization` `inr`	—	`snd_inr`
`inr_mul` 📖	mathematical	—	`inr` `MulZeroClass.toZero` `Unitization` `instMul` `MulZeroClass.toMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `SMulZeroClass.toSMul` `AddZero.toZero` `SMulWithZero.toSMulZeroClass`	—	`ext` `MulZeroClass.mul_zero` `zero_smul` `add_zero` `zero_add`
`inr_mul_inl` 📖	mathematical	—	`Unitization` `instMul` `MulZeroClass.toMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `inr` `inl`	—	`ext` `MulZeroClass.zero_mul` `smul_zero` `zero_add` `MulZeroClass.mul_zero` `add_zero` `inr_smul`
`inr_neg` 📖	mathematical	—	`inr` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Unitization` `instNeg` `NegZeroClass.toNeg`	—	`ext` `neg_zero`
`inr_smul` 📖	mathematical	—	`inr` `Unitization` `instSMul` `SMulZeroClass.toSMul`	—	`ext` `smul_zero`
`inr_star` 📖	mathematical	—	`inr` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Star.star` `Unitization` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar`	—	`ext` `star_zero`
`inr_sub` 📖	mathematical	—	`inr` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Unitization` `instSub`	—	`ext` `sub_zero`
`inr_zero` 📖	mathematical	—	`inr` `Unitization` `instZero`	—	—
`instCanLift` 📖	mathematical	—	`CanLift` `Unitization` `inr` `toProd`	—	`ext` `fst_inr`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `Unitization` `instSMul` `MulOpposite`	—	`Equiv.isCentralScalar` `Prod.isCentralScalar`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `Unitization` `instSMul`	—	`Equiv.isScalarTower` `Prod.isScalarTower`
`instIsStarNormal` 📖	mathematical	—	`IsStarNormal` `Unitization` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `inr`	—	`isStarNormal_inr`
`instNontrivialLeft` 📖	mathematical	—	`Nontrivial` `Unitization`	—	`Equiv.nontrivial` `nontrivial_prod_left`
`instNontrivialRight` 📖	mathematical	—	`Nontrivial` `Unitization`	—	`Equiv.nontrivial` `nontrivial_prod_right`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `Unitization` `instSMul`	—	`Equiv.smulCommClass` `Prod.smulCommClass`
`instStarModule` 📖	mathematical	—	`StarModule` `Unitization` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `StarRing.toStarAddMonoid` `instStar` `instSMul` `Algebra.toSMul` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`ext` `star_mul'` `StarModule.star_smul`
`isIdempotentElem_inr_iff` 📖	mathematical	—	`IsIdempotentElem` `Unitization` `instMul` `MulZeroClass.toMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `SMulZeroClass.toSMul` `AddZero.toZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `inr`	—	`inr_injective`
`isSelfAdjoint_inr` 📖	mathematical	—	`IsSelfAdjoint` `Unitization` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`inr_injective`
`isStarNormal_inr` 📖	mathematical	—	`IsStarNormal` `Unitization` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `inr`	—	`inr_injective`
`isStarProjection_inr_iff` 📖	mathematical	—	`IsStarProjection` `Unitization` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`lift_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `AlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `NonUnitalAlgHom.toAlgHom`	—	`IsScalarTower.left`
`lift_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AlgHom.funLike` `Equiv` `NonUnitalAlgHom` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `toProd` `NonUnitalAlgHom.instFunLike_1`	—	`IsScalarTower.left`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalAlgHom` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `NonUnitalAlgHom.comp` `NonUnitalAlgHomClass.toNonUnitalAlgHom` `AlgHom.funLike` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `inrNonUnitalAlgHom`	—	`IsScalarTower.left`
`lift_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalAlgHom.instFunLike_1` `Equiv` `AlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `AlgHom.funLike` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsScalarTower.left`
`linearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Unitization` `instAddCommMonoid` `Prod.instAddCommMonoid` `instModule` `Prod.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquiv` `toProd`	—	`RingHomInvPair.ids`
`linearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Unitization` `Prod.instAddCommMonoid` `instAddCommMonoid` `Prod.instModule` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquiv`	—	`RingHomInvPair.ids`
`linearMap_ext` 📖	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Unitization` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `inr`	—	—	`LinearEquiv.injective` `smulCommClass_self` `RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.prod_ext` `LinearMap.ext`
`linearMap_ext_iff` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Unitization` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `inr`	—	`linearMap_ext`
`mk_bijective` 📖	mathematical	—	`Function.Bijective` `Unitization`	—	`Equiv.bijective`
`mk_injective` 📖	mathematical	—	`Unitization`	—	`Equiv.injective`
`mk_surjective` 📖	mathematical	—	`Unitization`	—	`Equiv.surjective`
`mk_toProd` 📖	mathematical	—	`toProd`	—	—
`sndHom_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Unitization` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `sndHom` `toProd`	—	—
`snd_add` 📖	mathematical	—	`toProd` `Unitization` `instAdd`	—	—
`snd_inl` 📖	mathematical	—	`toProd` `inl`	—	—
`snd_inr` 📖	mathematical	—	`toProd` `inr`	—	—
`snd_mul` 📖	mathematical	—	`toProd` `Unitization` `instMul`	—	—
`snd_neg` 📖	mathematical	—	`toProd` `Unitization` `instNeg`	—	—
`snd_one` 📖	mathematical	—	`toProd` `Unitization` `instOne`	—	—
`snd_smul` 📖	mathematical	—	`toProd` `Unitization` `instSMul`	—	—
`snd_star` 📖	mathematical	—	`toProd` `Star.star` `Unitization` `instStar`	—	—
`snd_zero` 📖	mathematical	—	`toProd` `Unitization` `instZero`	—	—
`starAlgHom_ext` 📖	—	`NonUnitalStarAlgHom.comp` `Unitization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `instDistribMulAction` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instStar` `Algebra.toModule` `NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom` `StarAlgHom` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `StarAlgHom.instFunLike` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass` `inrNonUnitalStarAlgHom`	—	—	`IsScalarTower.left` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass` `algHom_ext''` `DFunLike.congr_fun`
`starAlgHom_ext_iff` 📖	mathematical	—	`NonUnitalStarAlgHom.comp` `Unitization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `instDistribMulAction` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instStar` `Algebra.toModule` `NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom` `StarAlgHom` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `StarAlgHom.instFunLike` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass` `inrNonUnitalStarAlgHom`	—	`IsScalarTower.left` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass` `starAlgHom_ext`
`starLift_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `StarAlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `starLift` `NonUnitalAlgHom.toAlgHom` `NonUnitalStarAlgHom.toNonUnitalAlgHom`	—	`IsScalarTower.left`
`starLift_apply_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `Equiv` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.toModule` `IsScalarTower.left` `DistribMulAction.toMulAction` `EquivLike.toFunLike` `Equiv.instEquivLike` `starLift` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `toProd` `NonUnitalStarAlgHom.instFunLike`	—	`IsScalarTower.left`
`starLift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `StarAlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `NonUnitalStarAlgHom` `Algebra.toModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `starLift` `NonUnitalStarAlgHom.comp` `StarAlgHom.toNonUnitalStarAlgHom` `inrNonUnitalStarAlgHom`	—	`IsScalarTower.left`
`starLift_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `NonUnitalStarAlgHom.instFunLike` `Equiv` `StarAlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `starLift` `StarAlgHom.instFunLike` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsScalarTower.left`
`starMap_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `starMap` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `toProd` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalStarAlgHom` `NonUnitalStarAlgHom.instFunLike`	—	`IsScalarTower.left`
`starMap_comp` 📖	mathematical	—	`starMap` `NonUnitalStarAlgHom.comp` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `StarAlgHom.comp` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `instStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`starAlgHom_ext` `IsScalarTower.left` `NonUnitalStarAlgHom.ext` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass` `ext` `starMap_inr`
`starMap_id` 📖	mathematical	—	`starMap` `NonUnitalStarAlgHom.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `StarAlgHom.id` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `instStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`starAlgHom_ext` `IsScalarTower.left` `NonUnitalStarAlgHom.ext` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass` `ext` `starMap_inr`
`starMap_injective` 📖	mathematical	`DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `NonUnitalStarAlgHom.instFunLike`	`Unitization` `DFunLike.coe` `StarAlgHom` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `starMap`	—	`IsScalarTower.left` `ext` `add_zero` `zero_add`
`starMap_inl` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `starMap` `inl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `add_zero`
`starMap_inr` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `starMap` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalStarAlgHom` `NonUnitalStarAlgHom.instFunLike`	—	`IsScalarTower.left` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_add`
`starMap_surjective` 📖	mathematical	`DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `NonUnitalStarAlgHom.instFunLike`	`Unitization` `DFunLike.coe` `StarAlgHom` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `starMap`	—	`ind` `IsScalarTower.left`
`toAddEquiv_linearEquiv` 📖	mathematical	—	`LinearEquiv.toAddEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Unitization` `instAddCommMonoid` `Prod.instAddCommMonoid` `instModule` `Prod.instModule` `linearEquiv` `addEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`RingHomInvPair.ids`
`toEquiv_addEquiv` 📖	mathematical	—	`AddEquiv.toEquiv` `Unitization` `instAdd` `Prod.instAdd` `addEquiv` `equiv`	—	—
`toProd_add` 📖	mathematical	—	`toProd` `Unitization` `instAdd` `Prod.instAdd`	—	—
`toProd_bijective` 📖	mathematical	—	`Function.Bijective` `Unitization` `toProd`	—	`Equiv.bijective`
`toProd_inj_iff` 📖	mathematical	—	`toProd`	—	`toProd_injective`
`toProd_injective` 📖	mathematical	—	`Unitization` `toProd`	—	`Equiv.injective`
`toProd_mk` 📖	mathematical	—	`toProd`	—	—
`toProd_neg` 📖	mathematical	—	`toProd` `Unitization` `instNeg` `Prod.instNeg`	—	—
`toProd_smul` 📖	mathematical	—	`toProd` `Unitization` `instSMul` `Prod.instSMul`	—	—
`toProd_surjective` 📖	mathematical	—	`Unitization` `toProd`	—	`Equiv.surjective`
`toProd_zero` 📖	mathematical	—	`toProd` `Unitization` `instZero` `Prod.instZero`	—	—

Unitization.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inr` 📖	mathematical	`IsIdempotentElem`	`IsIdempotentElem` `Unitization` `Unitization.instMul` `MulZeroClass.toMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `SMulZeroClass.toSMul` `AddZero.toZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `Unitization.inr`	—	`Unitization.isIdempotentElem_inr_iff`

---

← Back to Index