Porting note: added definition

[pitmonticone]

Classifies porting notes claiming anything equivalent to:

• "added definition"
• "new definition"

Examples

mathlib4/Mathlib/Data/Complex/Exponential.lean

Lines 198 to 203 in f0f609c

	-- Porting note: New definition
	/-- the exponential function as a monoid hom from `Multiplicative ℂ` to `ℂ` -/
	noncomputable def expMonoidHom : MonoidHom (Multiplicative ℂ) ℂ :=
	{ toFun := fun z => exp (Multiplicative.toAdd z),
	map_one' := by simp,
	map_mul' := by simp [exp_add] }

mathlib4/Mathlib/Data/Finset/Basic.lean

Lines 203 to 206 in f0f609c

	-- Porting note: new definition
	/-- Convert a finset to a set in the natural way. -/
	@[coe] def toSet (s : Finset α) : Set α :=
	{ a | a ∈ s }

mathlib4/Mathlib/Data/Sym/Basic.lean

Lines 46 to 49 in f0f609c

	-- Porting note: new definition
	/-- The canonical map to `Multiset α` that forgets that `s` has length `n` -/
	@[coe] def Sym.toMultiset {α : Type*} {n : ℕ} (s : Sym α n) : Multiset α :=
	s.1