## Stream: general

### Topic: putting algebra in mathlib

#### Johan Commelin (May 16 2020 at 09:21):

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 (May 16 2020 at 09:22):

@[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,
-- ^ error is here
| -[1+ m] -[1+ n] := show (((m + 1) * (n + 1) : ℕ) : α) = -(m + 1) * -(n + 1),


#### Johan Commelin (May 16 2020 at 09:22):

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 (May 16 2020 at 09:24):

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 (May 16 2020 at 09:24):

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

#### Johan Commelin (May 16 2020 at 09:24):

Thanks for rubberducking!

#### Johan Commelin (May 16 2020 at 10:04):

#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 (May 16 2020 at 10:05):

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 (May 16 2020 at 10:08):

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

#### Sebastien Gouezel (May 16 2020 at 10:08):

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 (May 16 2020 at 10:42):

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 (May 16 2020 at 11:38):

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 (May 16 2020 at 13:44):

@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 (May 16 2020 at 13:45):

Or am I missing something?

Last updated: Aug 03 2023 at 10:10 UTC