Skip to content

Commit 42e8bcd

Browse files
artie2000artie2000
authored
fix style
1 parent 5ece3c4 commit 42e8bcd

1 file changed

Lines changed: 1 addition & 2 deletions

File tree

‎Mathlib/Algebra/Group/Even.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,8 +47,7 @@ def IsSquare (a : α) : Prop := ∃ r, a = r * r
4747
@[to_additive]
4848
lemma isSquare_iff_exists_mul_self (a : α) : IsSquare a ↔ ∃ r, a = r * r := Iff.rfl
4949

50-
alias ⟨IsSquare.exists_mul_self, _⟩ := isSquare_iff_exists_mul_self
51-
attribute [to_additive] IsSquare.exists_mul_self
50+
@[to_additive] alias ⟨IsSquare.exists_mul_self, _⟩ := isSquare_iff_exists_mul_self
5251

5352
@[to_additive (attr := simp)] lemma IsSquare.mul_self (r : α) : IsSquare (r * r) := ⟨r, rfl⟩
5453

0 commit comments

Comments
 (0)