<commit_before>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import algebra.group.hom
import data.equiv.basic
/-!
# Type tags that turn additive structures into multiplicative, and vice versa

We define two type tags:

* `additive α`: turns any multiplicative structure on `α` into the corresponding
  additive structure on `additive α`;
* `multiplicative α`: turns any additive structure on `α` into the corresponding
  multiplicative structure on `multiplicative α`.

We also define instances `additive.*` and `multiplicative.*` that actually transfer the structures.
-/

universes u v
variables {α : Type u} {β : Type v}

/-- If `α` carries some multiplicative structure, then `additive α` carries the corresponding
additive structure. -/
def additive (α : Type*) := α
/-- If `α` carries some additive structure, then `multiplicative α` carries the corresponding
multiplicative structure. -/
def multiplicative (α : Type*) := α

/-- Reinterpret `x : α` as an element of `additive α`. -/
def additive.of_mul : α ≃ additive α := ⟨λ x, x, λ x, x, λ x, rfl, λ x, rfl⟩

/-- Reinterpret `x : additive α` as an element of `α`. -/
def additive.to_mul : additive α ≃ α := additive.of_mul.symm

/-- Reinterpret `x : α` as an element of `multiplicative α`. -/
def multiplicative.of_add : α ≃ multiplicative α := ⟨λ x, x, λ x, x, λ x, rfl, λ x, rfl⟩

/-- Reinterpret `x : multiplicative α` as an element of `α`. -/
def multiplicative.to_add : multiplicative α ≃ α := multiplicative.of_add.symm

@[simp] lemma to_add_of_add (x : α) : (multiplicative.of_add x).to_add = x := rfl
@[simp] lemma of_add_to_add (x : multiplicative α) : multiplicative.of_add x.to_add = x := rfl

@[simp] lemma to_mul_of_mul (x : α) : (additive.of_mul x).to_mul = x := rfl
@[simp] lemma of_mul_to_mul (x : additive α) : additive.of_mul x.to_mul = x := rfl

instance [inhabited α] : inhabited (additive α) := ⟨additive.of_mul (default α)⟩
instance [inhabited α] : inhabited (multiplicative α) := ⟨multiplicative.of_add (default α)⟩<commit_msg>chore(group/type_tags): Add missing simp lemmas (#4651)<commit_after>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import algebra.group.hom
import data.equiv.basic
/-!
# Type tags that turn additive structures into multiplicative, and vice versa

We define two type tags:

* `additive α`: turns any multiplicative structure on `α` into the corresponding
  additive structure on `additive α`;
* `multiplicative α`: turns any additive structure on `α` into the corresponding
  multiplicative structure on `multiplicative α`.

We also define instances `additive.*` and `multiplicative.*` that actually transfer the structures.
-/

universes u v
variables {α : Type u} {β : Type v}

/-- If `α` carries some multiplicative structure, then `additive α` carries the corresponding
additive structure. -/
def additive (α : Type*) := α
/-- If `α` carries some additive structure, then `multiplicative α` carries the corresponding
multiplicative structure. -/
def multiplicative (α : Type*) := α

namespace additive

/-- Reinterpret `x : α` as an element of `additive α`. -/
def of_mul : α ≃ additive α := ⟨λ x, x, λ x, x, λ x, rfl, λ x, rfl⟩

/-- Reinterpret `x : additive α` as an element of `α`. -/
def to_mul : additive α ≃ α := of_mul.symm

@[simp] lemma of_mul_symm_eq : (@of_mul α).symm = to_mul := rfl

@[simp] lemma to_mul_symm_eq : (@to_mul α).symm = of_mul := rfl

end additive

namespace multiplicative

/-- Reinterpret `x : α` as an element of `multiplicative α`. -/
def of_add : α ≃ multiplicative α := ⟨λ x, x, λ x, x, λ x, rfl, λ x, rfl⟩

/-- Reinterpret `x : multiplicative α` as an element of `α`. -/
def to_add : multiplicative α ≃ α := of_add.symm

@[simp] lemma of_add_symm_eq : (@of_add α).symm = to_add := rfl

@[simp] lemma to_add_symm_eq : (@to_add α).symm = of_add := rfl

end multiplicative

@[simp] lemma to_add_of_add (x : α) : (multiplicative.of_add x).to_add = x := rfl
@[simp] lemma of_add_to_add (x : multiplicative α) : multiplicative.of_add x.to_add = x := rfl

@[simp] lemma to_mul_of_mul (x : α) : (additive.of_mul x).to_mul = x := rfl
@[simp] lemma of_mul_to_mul (x : additive α) : additive.of_mul x.to_mul = x := rfl

instance [inhabited α] : inhabited (additive α) := ⟨additive.of_mul (default α)⟩
instance [inhabited α] : inhabited (multiplicative α) := ⟨multiplicative.of_add (default α)⟩
{'fraction_non_alphanumeric': 0.12477836879432624, 'fraction_numerical': 0.0035460992907801418, 'mean_word_length': 4.008879023307436, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5915649', 'n_tokens_mistral': 1740, 'n_tokens_neox': 1559, 'n_words': 590}