ULift

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

Statistics

Metric	Count
Definitions `addCommGroupWithOne`, `addCommMonoidWithOne`, `addGroupWithOne`, `addMonoidWithOne`, `commRing`, `commSemiring`, `distrib`, `instIntCast`, `instNatCast`, `mulZeroClass`, `nonAssocRing`, `nonAssocSemiring`, `nonUnitalCommRing`, `nonUnitalCommSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `nonUnitalRing`, `nonUnitalSemiring`, `ringEquiv`, `semiring`	20
Theorems `down_intCast`, `down_natCast`, `down_ofNat`, `up_intCast`, `up_natCast`, `up_ofNat`	6
Total	26

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	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`
`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	—
`nonUnitalCommRing` 📖	CompOp	—
`nonUnitalCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	1 math math: `instIsTopologicalRingULift`
`nonUnitalNonAssocSemiring` 📖	CompOp	1 math math: `instIsTopologicalSemiringULift`
`nonUnitalRing` 📖	CompOp	—
`nonUnitalSemiring` 📖	CompOp	—
`ringEquiv` 📖	CompOp	1 math math: `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`
`semiring` 📖	CompOp	3 math math: `algEquiv_apply`, `down_algebraMap`, `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