Mathlib Map

Theorems · Definition

Additive.toMul

{α : Type u} → Additive α ≃ α

Reinterpret x : Additive α as an element of α.

Defined in
Mathlib.Algebra.Group.TypeTags.Basic
Cited by
109 results in Mathlib
Foundations
Depth 11 from the axioms, rests on 42 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NumberField.Units.logEmbedding · cited by 25Units.logEmbeddingNumberField.Units.fundSystem · cited by 23Units.fundSystemMonoidHom.toAdditive · cited by 19MonoidHom.toAdditiveNat.finMulAntidiag · cited by 13Nat.finMulAntidiagAddMonoidHom.toMultiplicativeRight · cited by 9AddMonoidHom.toMultiplica…groupCohomology.cocycles₁IsoOfIsTrivial · cited by 7groupCohomology.cocycles₁…Nat.mem_finMulAntidiag · cited by 7Nat.mem_finMulAntidiagSubmonoid.toAddSubmonoid · cited by 5Submonoid.toAddSubmonoidSubgroup.strictWidthInfty_pos_iff · cited by 5Subgroup.strictWidthInfty…AddMonoidHom.toMultiplicativeLeft · cited by 5AddMonoidHom.toMultiplica…Valuation.ofAddValuation · cited by 5Valuation.ofAddValuationValuation.toAddValuation · cited by 5Valuation.toAddValuationZMod.AddAutEquivUnits · cited by 4ZMod.AddAutEquivUnitsAdditive.ext · cited by 4Additive.extAddEquiv.prodAdditive · cited by 4AddEquiv.prodAdditiveEquiv · cited by 8337EquivEquiv.symm · cited by 3681Equiv.symmAdditive · cited by 356AdditiveAdditive.ofMul · cited by 155Additive.ofMulAdditive.toMulCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by125

Results whose statement or proof uses this declaration.