toAdditive

📁 Source: MathlibTest/toAdditive.lean

Statistics

Metric	Count
Definitions toAdditive, toAdditive, toAdditive, toAdditive, toAdditive	5
Theorems	0
Total	5

MonoidAlgebra

Definitions

Name	Category	Theorems
toAdditive 📖	CompOp	—

MonoidHom

Definitions

Name	Category	Theorems
toAdditive 📖	CompOp	20 math math: toAdditive_apply_apply, MulEquiv.toAdditive_apply_apply, toAdditive_symm_apply_apply, AddMonCat.equivalence_inverse_map, AddMonCat.equivalence_counitIso, FreeAbelianGroup.liftAddEquiv_symm_apply, GrpCat.toAddGrp_map, coe_toAdditive_map, MulEquiv.toAdditive_symm_apply_apply, coe_toAdditive_range, toAdditive_id, coe_toAdditive, Subgroup.toAddSubgroup_comap, MulEquiv.toAdditive_symm_apply_symm_apply, MulEquiv.toAdditive_apply_symm_apply, AddCommMonCat.equivalence_counitIso, AddCommMonCat.equivalence_inverse_map, coe_toMultiplicative, CommGrpCat.toAddCommGrp_map, coe_toAdditive_ker

MulEquiv

Definitions

Name	Category	Theorems
toAdditive 📖	CompOp	4 math math: toAdditive_apply_apply, toAdditive_symm_apply_apply, toAdditive_symm_apply_symm_apply, toAdditive_apply_symm_apply

OrderMonoidIso

Definitions

Name	Category	Theorems
toAdditive 📖	CompOp	—

Rep

Definitions

Name	Category	Theorems
toAdditive 📖	CompOp	3 math math: toAdditive_symm_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, toAdditive_apply

---

← Back to Index