PUnit

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

Statistics

Metric	Count
Definitions addCommGroup, commGroup, instAdd_mathlib, instDiv_mathlib, instInv_mathlib, instMul_mathlib, instNeg_mathlib, instOne_mathlib, instSub_mathlib, instZero_mathlib	10
Theorems add_eq, div_eq, inv_eq, mul_eq, neg_eq, one_eq, sub_eq, zero_eq	8
Total	18

PUnit

Definitions

Name	Category	Theorems
addCommGroup 📖	CompOp	81 math math: CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj, AddEquiv.coprodPUnit_symm_apply, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso_inv_app_hom_app, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso_hom_app_hom_app, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_X, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_mul, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor, isOrderedCancelAddMonoid, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_μ, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app, AddEquiv.coprodPUnit_apply, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_addMon_zero, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_laxMonoidalToAddMon_obj_zero, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_map_hom, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon_obj, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_addMon_add, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ, AddEquiv.punitCoprod_symm_apply, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_X, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_map, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app, CliffordAlgebraRing.ι_eq_zero, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ, CliffordAlgebraRing.involute_eq_id, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_laxMonoidalToAddMon_obj_add, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_obj, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_map_hom_app, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_map_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app, CliffordAlgebraRing.reverse_apply, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon_map, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_map, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_one, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_ε, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj, CliffordAlgebraRing.reverse_eq_id, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul, CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.isAddMonHom_counitIsoAux, CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app, AddEquiv.punitCoprod_apply, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app
commGroup 📖	CompOp	18 math math: CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso, MulEquiv.coprodPUnit_symm_apply, MulEquiv.coprodPUnit_apply, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse, MulEquiv.punitCoprod_symm_apply, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one, MulEquiv.punitCoprod_apply, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso
instAdd_mathlib 📖	CompOp	2 math math: add_eq, canonicallyOrderedAdd
instDiv_mathlib 📖	CompOp	1 math math: div_eq
instInv_mathlib 📖	CompOp	1 math math: inv_eq
instMul_mathlib 📖	CompOp	2 math math: instIsCancelMulZero, mul_eq
instNeg_mathlib 📖	CompOp	1 math math: neg_eq
instOne_mathlib 📖	CompOp	1 math math: one_eq
instSub_mathlib 📖	CompOp	1 math math: sub_eq
instZero_mathlib 📖	CompOp	2 math math: zero_eq, instIsCancelMulZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq 📖	mathematical	—	instAdd_mathlib	—	—
div_eq 📖	mathematical	—	instDiv_mathlib	—	—
inv_eq 📖	mathematical	—	instInv_mathlib	—	—
mul_eq 📖	mathematical	—	instMul_mathlib	—	—
neg_eq 📖	mathematical	—	instNeg_mathlib	—	—
one_eq 📖	mathematical	—	instOne_mathlib	—	—
sub_eq 📖	mathematical	—	instSub_mathlib	—	—
zero_eq 📖	mathematical	—	instZero_mathlib	—	—

---

← Back to Index