Classifies porting notes claiming anything semantically equivalent to:
- "added theorem"
- "added theorems"
- "new theorem"
- "new theorems"
- "added lemma"
- "new lemma"
- "new lemmas"
Examples
|
-- porting note: added |
|
lemma coe_id {X : GroupWithZeroCat} : (𝟙 X : X → X) = id := rfl |
|
|
|
-- porting note: added |
|
lemma coe_comp {X Y Z : GroupWithZeroCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl |
|
-- Porting note: new |
|
@[to_additive (attr := simp)] |
|
theorem lift_ofList (f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod := |
|
prodAux_eq _ |
|
-- 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 _ |
|
-- 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 _ _ _ |
|
|
|
-- 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⟩ |
