fix(data/sigma/basic): rename ext to sigma.ext (#3916)

leanprover-community · Aug 23, 2020 · 7d88a30 · 7d88a30
1 parent ff97055
commit 7d88a30
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/sigma/basic.lean b/src/data/sigma/basic.lean
@@ -34,7 +34,7 @@ by simp
 | ⟨i, x⟩ := rfl
 
 @[ext]
-lemma ext {x₀ x₁ : sigma β}
+lemma sigma.ext {x₀ x₁ : sigma β}
   (h₀ : x₀.1 = x₁.1)
   (h₁ : x₀.1 = x₁.1 → x₀.2 == x₁.2) :
   x₀ = x₁ :=