# Zulip Chat Archive

## 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,
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 (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: May 18 2021 at 17:44 UTC