Lift

📁 Source: Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean

Statistics

Metric	Count
Definitions `domCongr`, `domCongrAlg`, `domLCongr`, `equivMapDomain`, `liftNCAlgHom`, `mapDomainAlgHom`, `submoduleOfSmulMem`	7
Theorems `coeff_equivMapDomain`, `domCongrAlg_apply`, `domCongrAlg_toAlgHom`, `domCongr_apply`, `domCongr_refl`, `domCongr_single`, `domCongr_support`, `domCongr_symm`, `equivMapDomain_eq_mapDomain`, `equivMapDomain_refl`, `equivMapDomain_single`, `equivMapDomain_trans`, `lift_apply`, `lift_apply'`, `lift_def`, `lift_of`, `lift_single`, `lift_symm_apply`, `lift_unique`, `lift_unique'`, `mapDomainAlgHom_apply`, `toFinsupp_equivMapDomain`	22
Total	29

SkewMonoidAlgebra

Definitions

Name	Category	Theorems
`domCongr` 📖	CompOp	1 math math: `domCongr_apply`
`domCongrAlg` 📖	CompOp	6 math math: `domCongr_support`, `domCongrAlg_apply`, `domCongrAlg_toAlgHom`, `domCongr_refl`, `domCongr_single`, `domCongr_symm`
`domLCongr` 📖	CompOp	—
`equivMapDomain` 📖	CompOp	7 math math: `equivMapDomain_refl`, `coeff_equivMapDomain`, `toFinsupp_equivMapDomain`, `equivMapDomain_trans`, `domCongr_apply`, `equivMapDomain_eq_mapDomain`, `equivMapDomain_single`
`liftNCAlgHom` 📖	CompOp	—
`mapDomainAlgHom` 📖	CompOp	2 math math: `domCongrAlg_toAlgHom`, `mapDomainAlgHom_apply`
`submoduleOfSmulMem` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_equivMapDomain` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `equivMapDomain` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`domCongrAlg_apply` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AlgEquiv` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSemiring` `instAlgebraOfSMulCommClass` `AlgEquiv.instFunLike` `domCongrAlg` `MulEquiv.symm`	—	—
`domCongrAlg_toAlgHom` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	`AlgEquiv.toAlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `domCongrAlg` `mapDomainAlgHom` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`	—	`AlgHom.ext` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `equivMapDomain_eq_mapDomain`
`domCongr_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `domCongr` `equivMapDomain`	—	—
`domCongr_refl` 📖	mathematical	—	`domCongrAlg` `MulEquiv.refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `AlgEquiv.refl` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instAlgebraOfSMulCommClass`	—	`AlgEquiv.ext` `ext`
`domCongr_single` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	`AlgEquiv` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `AlgEquiv.instFunLike` `domCongrAlg` `single` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`equivMapDomain_single`
`domCongr_support` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	`support` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AlgEquiv` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSemiring` `instAlgebraOfSMulCommClass` `AlgEquiv.instFunLike` `domCongrAlg` `Finset.map` `Equiv.toEmbedding` `EquivLike.toEquiv`	—	—
`domCongr_symm` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	`AlgEquiv.symm` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `domCongrAlg` `MulEquiv.symm`	—	—
`equivMapDomain_eq_mapDomain` 📖	mathematical	—	`equivMapDomain` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`toFinsupp_injective` `Finsupp.ext` `toFinsupp_mapDomain` `Finsupp.mapDomain_equiv_apply`
`equivMapDomain_refl` 📖	mathematical	—	`equivMapDomain` `Equiv.refl`	—	`ext`
`equivMapDomain_single` 📖	mathematical	—	`equivMapDomain` `single` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`toFinsupp_injective` `Finsupp.equivMapDomain_single`
`equivMapDomain_trans` 📖	mathematical	—	`equivMapDomain` `Equiv.trans`	—	`ext`
`lift_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toSMul` `MonoidHom.instFunLike`	—	`Algebra.smul_def`
`lift_apply'` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `MonoidHom.instFunLike`	—	—
`lift_def` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `algebraMap` `MonoidHom.instFunLike`	—	—
`lift_of` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `instNonAssocSemiring` `MonoidHom.instFunLike` `of`	—	`of_apply` `lift_symm_apply` `Equiv.symm_apply_apply`
`lift_single` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `single` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toSMul` `MonoidHom.instFunLike`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `lift_def` `liftNC_single` `Algebra.smul_def` `AddMonoidHom.coe_coe`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `Equiv` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `AlgHom.funLike` `single` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`lift_unique` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toSMul` `single` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `lift_unique'` `lift_apply` `of_apply`
`lift_unique'` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `MonoidHom.comp` `instNonAssocSemiring` `MonoidHomClass.toMonoidHom` `AlgHom.funLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `of`	—	`Equiv.apply_symm_apply`
`mapDomainAlgHom_apply` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe`	`AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `AlgHom.funLike` `mapDomainAlgHom` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `single`	—	—
`toFinsupp_equivMapDomain` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `equivMapDomain` `Finsupp.equivMapDomain`	—	—

---

← Back to Index