Porting note: added theorem

[pitmonticone]

Classifies porting notes claiming anything equivalent to:

• "added theorem"
• "added theorems"
• "new theorem"
• "new theorems"

Examples

mathlib4/Mathlib/Algebra/FreeMonoid/Basic.lean

Lines 234 to 237 in bad9e36

	-- Porting note: new
	@[to_additive (attr := simp)]
	theorem lift_ofList (f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod :=
	prodAux_eq _

mathlib4/Mathlib/Algebra/Star/Basic.lean

Lines 341 to 345 in bad9e36

	-- Porting note: new theorem
	@[simp]
	theorem star_ofNat [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] :
	star (no_index (OfNat.ofNat n) : R) = OfNat.ofNat n :=
	star_natCast _

mathlib4/Mathlib/Analysis/Normed/Group/AddTorsor.lean

Lines 146 to 150 in bad9e36

	-- Porting note: new
	@[simp]
	theorem nndist_vsub_cancel_left (x y z : P) : nndist (x -ᵥ y) (x -ᵥ z) = nndist y z :=
	NNReal.eq <| dist_vsub_cancel_left _ _ _

mathlib4/Mathlib/Data/Fintype/Card.lean

Lines 640 to 650 in bad9e36

	-- Porting note: new theorem
	theorem surjective_of_injective {f : α → α} (hinj : Injective f) : Surjective f := by
	intro x
	have := Classical.propDecidable
	cases nonempty_fintype α
	have h₁ : image f univ = univ :=
	eq_of_subset_of_card_le (subset_univ _)
	((card_image_of_injective univ hinj).symm ▸ le_rfl)
	have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
	obtain ⟨y, h⟩ := mem_image.1 h₂
	exact ⟨y, h.2⟩

[pitmonticone]

Joined with #10756.