Theorems · Theorem · group theory
monoidEndToAdditive_apply_apply
∀ (M : Type u_4) [inst : MulOneClass M] (f : M →* M) (a : Additive M), ((monoidEndToAdditive M) f) a = Additive.ofMul (f (Additive.toMul a))
- Defined in
- Mathlib.Algebra.Group.Equiv.TypeTags
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
- Assumes
- MulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Equivstatement · cited by 8,337
- MonoidHomstatement and proof · cited by 3,629
- AddMonoidHomstatement · cited by 3,230
- MulEquivstatement · cited by 1,142
- MulOneClassstatement and proof · cited by 1,018
- Additivestatement and proof · cited by 356
- Additive.ofMulstatement · cited by 155
- Additive.toMulstatement · cited by 109
- AddMonoid.Endstatement · cited by 64
- Monoid.Endstatement · cited by 16
- monoidEndToAdditivestatement and proof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.