PUnit

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

Statistics

Metric	Count
Definitions commRing	1
Theorems instIsCancelMulZero	1
Total	2

PUnit

Definitions

Name	Category	Theorems
commRing 📖	CompOp	16 math math: norm_unit_eq, Submodule.botEquivPUnit_apply, IsNoetherian.equivPUnitOfProdInjective_apply, Submodule.botEquivPUnit_symm_apply, lcm_eq, rank_punit, CliffordAlgebraRing.ι_eq_zero, CliffordAlgebraRing.involute_eq_id, gcd_eq, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.empty_presheaf, CliffordAlgebraRing.reverse_apply, Algebra.algebraMap_pUnit, CliffordAlgebraRing.reverse_eq_id, AlgebraicGeometry.spec_punit_isEmpty, IsNoetherian.equivPUnitOfProdInjective_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCancelMulZero 📖	mathematical	—	IsCancelMulZero instMul_mathlib instZero_mathlib	—	—

---

← Back to Index