putting algebra in mathlib

Stream: general

[Johan Commelin]

I'm trying to put the algebra from core back into mathlib.
I'm hitting an error in data/int/basic:

1 goal
α : Type u_1,
_inst_1 : ring α,
cast_mul : ∀ (m n : ℤ), ↑(m * n) = ↑m * ↑n,
m n : ℕ
⊢ -↑((m + 1) * n) = -(↑m + 1) * ↑n
basic.lean:1193:5: error
rewrite tactic failed, did not find instance of the pattern in the target expression
  -(?m_1 * ?m_2)
state:
α : Type u_1,
_inst_1 : ring α,
cast_mul : ∀ (m n : ℤ), ↑(m * n) = ↑m * ↑n,
m n : ℕ
⊢ -((↑m + 1) * ↑n) = -(↑m + 1) * ↑n

[Johan Commelin]

@[simp, norm_cast] theorem cast_mul [ring α] : ∀ m n, ((m * n : ℤ) : α) = m * n
| (m : ℕ) (n : ℕ) := nat.cast_mul _ _
| (m : ℕ) -[1+ n] := (cast_neg_of_nat _).trans $
  show (-(m * (n + 1) : ℕ) : α) = m * -(n + 1),
  by rw [nat.cast_mul, nat.cast_add_one, neg_mul_eq_mul_neg]
| -[1+ m] (n : ℕ) := (cast_neg_of_nat _).trans $
  show (-((m + 1) * n : ℕ) : α) = -(m + 1) * n,
  by rw [nat.cast_mul, nat.cast_add_one, neg_mul_eq_neg_mul]
  -- ^ error is here
| -[1+ m] -[1+ n] := show (((m + 1) * (n + 1) : ℕ) : α) = -(m + 1) * -(n + 1),
  by rw [nat.cast_mul, nat.cast_add_one, nat.cast_add_one, neg_mul_neg]

[Johan Commelin]

Of course I can fix it. But I'm trying to understand where the error came from in the first place. I would rather fix the root issue.

[Johan Commelin]

Ooh, never mind... that line has neg_mul_eq_neg_mul :face_palm:
which is not the same as neg_mul_eq_mul_neg

[Johan Commelin]

So I need to make more things protected. (-;

[Johan Commelin]

Thanks for rubberducking!

[Johan Commelin]

#2697 puts algebra back in mathlib (this depends on a new lean release). Currently the branch builds number_theory/quadratic_reciprocity without errors.

[Johan Commelin]

There are some errors in category_theory, but I think this is due to other changes in the newest version of lean.

[Yury G. Kudryashov]

Is there some nightly/hourly/whatever version of lean that we can put into leanpkg.toml instead of local?

[Sebastien Gouezel]

This means we will be able to remove the simp attribute on one_div_eq_inv, among many many other things. Thanks so much!

[Johan Commelin]

A second iteration of this might also move the order hierarchy out of core. I didn't do that now, because I don't really have a need for it. And I wanted to keep this "small" (-;
Yes, I'm excited about all the tiny little fixes that we can now start making.

[Yury G. Kudryashov]

We still have

/-- this is needed for compatibility between Lean 3.4.2 and Lean 3.5.1c -/
def has_div_of_division_ring [division_ring α] : has_div α := division_ring_has_div

in algebra/ring

[Johan Commelin]

@Yury G. Kudryashov Sorry, I'm slow. What is your point? I've moved everything out of core, right? So this is stuff that we can now leisurely fix.

[Johan Commelin]

Or am I missing something?