ULift

📁 Source: Mathlib/Algebra/Ring/ULift.lean

Statistics

Metric	Count
Definitions `ulift`, `addCommGroupWithOne`, `addCommMonoidWithOne`, `addGroupWithOne`, `addMonoidWithOne`, `commRing`, `commSemiring`, `distrib`, `instIntCast`, `instNatCast`, `mulZeroClass`, `nonAssocRing`, `nonAssocSemiring`, `nonUnitalCommRing`, `nonUnitalCommSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `nonUnitalRing`, `nonUnitalSemiring`, `ringEquiv`, `semiring`	21
Theorems `comp_ulift_eq`, `down_ulift_apply`, `ulift_apply`, `down_intCast`, `down_natCast`, `down_ofNat`, `up_intCast`, `up_natCast`, `up_ofNat`	9
Total	30

RingHom

Definitions

Name	Category	Theorems
`ulift` 📖	CompOp	3 math math: `down_ulift_apply`, `comp_ulift_eq`, `ulift_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_ulift_eq` 📖	mathematical	—	`comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ULift.nonAssocSemiring` `RingEquiv.toRingHom` `ULift.ringEquiv` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ulift` `RingEquiv.symm` `ULift.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `ULift.add` `Distrib.toAdd`	—	—
`down_ulift_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `ULift.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike` `ulift`	—	—
`ulift_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `ULift.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFunLike` `ulift`	—	—

ULift

Definitions

Name	Category	Theorems
`addCommGroupWithOne` 📖	CompOp	—
`addCommMonoidWithOne` 📖	CompOp	—
`addGroupWithOne` 📖	CompOp	—
`addMonoidWithOne` 📖	CompOp	1 math math: `charP`
`commRing` 📖	CompOp	8 math math: `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply`, `AlgebraicGeometry.AffineSpace.over_over`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly`
`commSemiring` 📖	CompOp	11 math math: `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly`, `algebraMap_apply'`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply`, `AlgebraicGeometry.AffineSpace.over_over`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly`, `AlgHom.down_ulift_apply`, `AlgHom.ulift_apply`
`distrib` 📖	CompOp	—
`instIntCast` 📖	CompOp	2 math math: `up_intCast`, `down_intCast`
`instNatCast` 📖	CompOp	2 math math: `up_natCast`, `down_natCast`
`mulZeroClass` 📖	CompOp	—
`nonAssocRing` 📖	CompOp	—
`nonAssocSemiring` 📖	CompOp	3 math math: `RingHom.down_ulift_apply`, `RingHom.comp_ulift_eq`, `RingHom.ulift_apply`
`nonUnitalCommRing` 📖	CompOp	—
`nonUnitalCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	1 math math: `instIsTopologicalRingULift`
`nonUnitalNonAssocSemiring` 📖	CompOp	1 math math: `instIsTopologicalSemiringULift`
`nonUnitalRing` 📖	CompOp	—
`nonUnitalSemiring` 📖	CompOp	—
`ringEquiv` 📖	CompOp	2 math math: `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`, `RingHom.comp_ulift_eq`
`semiring` 📖	CompOp	7 math math: `algEquiv_apply`, `algEquiv_symm_apply`, `down_algebraMap`, `down_algEquiv_symm_apply`, `AlgHom.down_ulift_apply`, `AlgHom.ulift_apply`, `algebraMap_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_intCast` 📖	mathematical	—	`instIntCast`	—	—
`down_natCast` 📖	mathematical	—	`instNatCast`	—	—
`down_ofNat` 📖	—	—	—	—	—
`up_intCast` 📖	mathematical	—	`instIntCast`	—	—
`up_natCast` 📖	mathematical	—	`instNatCast`	—	—
`up_ofNat` 📖	—	—	—	—	—

---

← Back to Index