Documentation Verification Report

Unitization

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

Statistics

Metric	Count
Definitions `unitization`, `unitizationStarAlgEquiv`, `unitization`, `unitizationAlgEquiv`, `unitization`, `unitization`	6
Theorems `unitization_injective`, `unitization_injective'`, `unitizationStarAlgEquiv_apply_coe`, `unitization_apply`, `unitization_injective`, `unitization_range`, `unitizationAlgEquiv_apply_coe`, `unitization_apply`, `unitization_injective`, `unitization_range`, `unitization_apply`, `unitization_range`, `unitization_apply`, `unitization_range`, `lift_range`, `lift_range_le`, `starLift_range`, `starLift_range_le`	18
Total	24

AlgHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitization_injective` 📖	—	`SetLike.instMembership` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `Unitization` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	—	`NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `NonUnitalSubringClass.addSubgroupClass` `IsScalarTower.left` `unitization_injective'` `SMulMemClass.smul_mem` `Algebra.algebraMap_eq_smul_one` `inv_smul_smul₀`
`unitization_injective'` 📖	—	`SetLike.instMembership` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `Unitization` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—	`NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `NonUnitalSubringClass.addSubgroupClass` `IsScalarTower.left` `injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Unitization.ind` `add_eq_zero_iff_eq_neg` `Unitization.ext` `neg_zero` `AddSubmonoidClass.toZeroMemClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `commutes` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `NegMemClass.neg_mem` `NonUnitalSubringClass.toNegMemClass`

NonUnitalStarSubalgebra

Definitions

Name	Category	Theorems
`unitization` 📖	CompOp	3 math math: `unitization_range`, `unitization_injective`, `unitization_apply`
`unitizationStarAlgEquiv` 📖	CompOp	1 math math: `unitizationStarAlgEquiv_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitizationStarAlgEquiv_apply_coe` 📖	mathematical	`SetLike.instMembership` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`StarSubalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `StarSubalgebra.setLike` `StarAlgebra.adjoin` `SetLike.coe` `DFunLike.coe` `StarAlgEquiv` `Unitization` `Unitization.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSubringClass.toNonUnitalRing` `Ring.toNonUnitalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubringClass.toRing` `StarSubalgebra.subringClass` `Unitization.instMul` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SubmoduleClass.module` `Algebra.toModule` `NonUnitalSubringClass.addSubgroupClass` `Unitization.instSMul` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `SubsemiringClass.toSemiring` `StarSubalgebra.subsemiringClass` `StarSubalgebra.algebra` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `StarMemClass.instStar` `StarSubalgebra.starMemClass` `StarAlgEquiv.instFunLike` `unitizationStarAlgEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom` `RingHom.instFunLike` `algebraMap` `Unitization.fst` `Unitization.snd`	—	`StarSubalgebra.subringClass` `NonUnitalSubringClass.addSubgroupClass` `StarSubalgebra.subsemiringClass` `StarSubalgebra.starMemClass`
`unitization_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Unitization` `SetLike.instMembership` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `SubmoduleClass.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `Unitization.instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarMemClass.instStar` `StarAlgHom.instFunLike` `unitization` `Distrib.toAdd` `RingHom` `RingHom.instFunLike` `algebraMap` `Unitization.fst` `Unitization.snd`	—	`NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left`
`unitization_injective` 📖	mathematical	`SetLike.instMembership` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`Unitization` `DFunLike.coe` `StarAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubmoduleClass.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `Unitization.instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarMemClass.instStar` `StarAlgHom.instFunLike` `unitization`	—	`AlgHomClass.unitization_injective` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left` `StarAlgHom.instAlgHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_add`
`unitization_range` 📖	mathematical	—	`StarAlgHom.range` `Unitization` `SetLike.instMembership` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `SubmoduleClass.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `Unitization.instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `Unitization.instStarRing` `StarMemClass.instStarRing` `StarMemClass.instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarMul.toInvolutiveStar` `StarRing.toStarMul` `unitization` `StarAlgebra.adjoin` `SetLike.coe`	—	`NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left` `StarMemClass.instStarModule` `unitization.eq_1` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `Unitization.starLift_range` `NonUnitalStarAlgHom.coe_range` `Subtype.range_coe_subtype`

NonUnitalSubalgebra

Definitions

Name	Category	Theorems
`unitization` 📖	CompOp	3 math math: `unitization_injective`, `unitization_range`, `unitization_apply`
`unitizationAlgEquiv` 📖	CompOp	1 math math: `unitizationAlgEquiv_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitizationAlgEquiv_apply_coe` 📖	mathematical	`SetLike.instMembership` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `SetLike.coe` `DFunLike.coe` `AlgEquiv` `Unitization` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubmoduleClass.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `Subalgebra.toSemiring` `Unitization.instAlgebra` `Algebra.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSubringClass.toNonUnitalRing` `Ring.toNonUnitalRing` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalSubringClass.addSubgroupClass` `IsScalarTower.left` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `Subalgebra.algebra` `AlgEquiv.instFunLike` `unitizationAlgEquiv` `Distrib.toAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom` `RingHom.instFunLike` `algebraMap` `Unitization.fst` `Unitization.snd`	—	`NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `NonUnitalSubringClass.addSubgroupClass` `IsScalarTower.left`
`unitization_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Unitization` `SetLike.instMembership` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `SubmoduleClass.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `Unitization.instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AlgHom.funLike` `unitization` `Distrib.toAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom` `RingHom.instFunLike` `algebraMap` `Unitization.fst` `Unitization.snd`	—	`NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left`
`unitization_injective` 📖	mathematical	`SetLike.instMembership` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`Unitization` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubmoduleClass.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `Unitization.instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AlgHom.funLike` `unitization`	—	`AlgHomClass.unitization_injective` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left` `AlgHom.algHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_add`
`unitization_range` 📖	mathematical	—	`AlgHom.range` `Unitization` `SetLike.instMembership` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `SubmoduleClass.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `Unitization.instAlgebra` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `unitization` `Algebra.adjoin` `SetLike.coe`	—	`NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left` `unitization.eq_1` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `Unitization.lift_range` `NonUnitalAlgHom.coe_range` `Subtype.range_coe_subtype`

NonUnitalSubring

Definitions

Name	Category	Theorems
`unitization` 📖	CompOp	2 math math: `unitization_apply`, `unitization_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitization_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Unitization` `SetLike.instMembership` `Int.instCommSemiring` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toIntModule` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSubringClass.toNonUnitalRing` `Ring.toNonUnitalRing` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `AddCommGroup.toAddGroup` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Unitization.instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.intIsScalarTower` `Int.instRing` `Ring.toIntAlgebra` `AlgHom.funLike` `unitization` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Unitization.fst` `Unitization.snd`	—	`NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `AddCommGroup.intIsScalarTower`
`unitization_range` 📖	mathematical	—	`AlgHom.range` `Unitization` `SetLike.instMembership` `Int.instCommSemiring` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toIntModule` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSubringClass.toNonUnitalRing` `Ring.toNonUnitalRing` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `AddCommGroup.toAddGroup` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Unitization.instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.intIsScalarTower` `Int.instRing` `Ring.toIntAlgebra` `unitization` `subalgebraOfSubring` `Subring.closure` `SetLike.coe`	—	`AddSubgroupClass.zsmulMemClass` `NonUnitalSubringClass.addSubgroupClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `NonUnitalNonAssocRing.int_isScalarTower` `AddGroup.int_smulCommClass` `AddCommGroup.intIsScalarTower` `unitization.eq_1` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left` `NonUnitalSubalgebra.unitization_range` `Algebra.adjoin_int`

NonUnitalSubsemiring

Definitions

Name	Category	Theorems
`unitization` 📖	CompOp	2 math math: `unitization_apply`, `unitization_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitization_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Unitization` `SetLike.instMembership` `Nat.instCommSemiring` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `AddCommMonoid.toNatModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toDistribSMul` `Unitization.instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `AddCommMonoid.nat_isScalarTower` `Nat.instSemiring` `Semiring.toNatAlgebra` `AlgHom.funLike` `unitization` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Unitization.fst` `Unitization.snd`	—	`NonUnitalNonAssocSemiring.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `AddCommMonoid.nat_isScalarTower`
`unitization_range` 📖	mathematical	—	`AlgHom.range` `Unitization` `SetLike.instMembership` `Nat.instCommSemiring` `Unitization.instSemiring` `NonUnitalSubsemiringClass.toNonUnitalSemiring` `Semiring.toNonUnitalSemiring` `AddCommMonoid.toNatModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toDistribSMul` `Unitization.instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `AddCommMonoid.nat_isScalarTower` `Nat.instSemiring` `Semiring.toNatAlgebra` `unitization` `subalgebraOfSubsemiring` `Subsemiring.closure` `Semiring.toNonAssocSemiring` `SetLike.coe`	—	`AddSubmonoidClass.nsmulMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalNonAssocSemiring.nat_isScalarTower` `AddMonoid.nat_smulCommClass` `AddCommMonoid.nat_isScalarTower` `unitization.eq_1` `SetLike.instIsScalarTower` `NonUnitalSubsemiringClass.mulMemClass` `IsScalarTower.right` `SetLike.instSMulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.left` `NonUnitalSubalgebra.unitization_range` `Algebra.adjoin_nat`

Unitization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_range` 📖	mathematical	—	`AlgHom.range` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `NonUnitalAlgHom` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Algebra.adjoin` `SetLike.coe` `NonUnitalSubalgebra` `NonUnitalSubalgebra.instSetLike` `NonUnitalAlgHom.range` `NonUnitalAlgHom.instFunLike_1` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass`	—	`eq_of_forall_ge_iff` `IsScalarTower.left` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `lift_range_le` `Algebra.adjoin_le_iff`
`lift_range_le` 📖	mathematical	—	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `AlgHom.range` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `NonUnitalAlgHom` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `NonUnitalSubalgebra` `NonUnitalSubalgebra.instPartialOrder` `NonUnitalAlgHom.range` `NonUnitalAlgHom.instFunLike_1` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `Subalgebra.toNonUnitalSubalgebra`	—	`IsScalarTower.left` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_add` `ind` `add_zero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSMulMemClass`
`starLift_range` 📖	mathematical	—	`StarAlgHom.range` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStarRing` `DFunLike.coe` `Equiv` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `StarAlgHom` `instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `starLift` `StarAlgebra.adjoin` `SetLike.coe` `NonUnitalStarSubalgebra` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgHom.range` `NonUnitalStarAlgHom.instFunLike` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass`	—	`eq_of_forall_ge_iff` `IsScalarTower.left` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `starLift_range_le` `StarAlgebra.adjoin_le_iff`
`starLift_range_le` 📖	mathematical	—	`StarSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `StarSubalgebra.instPartialOrder` `StarAlgHom.range` `Unitization` `instSemiring` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instStarRing` `DFunLike.coe` `Equiv` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `StarAlgHom` `instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `starLift` `NonUnitalStarSubalgebra` `NonUnitalStarSubalgebra.instPartialOrder` `NonUnitalStarAlgHom.range` `NonUnitalStarAlgHom.instFunLike` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `StarSubalgebra.toNonUnitalStarSubalgebra`	—	`IsScalarTower.left` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_add` `ind` `add_zero` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `StarSubalgebra.subsemiringClass` `algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `StarSubalgebra.smulMemClass`

---

← Back to Index