My favorite group lemma

Stream: general

[orlando cau]

Hello I'm a beginner

I don't understand i how to prove my favorite group lemma :D Can anyone help me ?

example(G : Type)[group G] :((∀ c : G,  c = c⁻¹)  → (∀ a b : G, a*b = b*a)):=
begin
    intro h,
    intros a b,
    calc
        a*b = (a*b)⁻¹  : h (a*b)
        ... = b⁻¹ *a⁻¹ : by  rw mul_inv_rev
        ... = b*a⁻¹    : sorry
        ... = b*a      : sorry
end
Edit : thx Donald

[Donald Sebastian Leung]

orlando cau said:

Hello I'm a beginner

I don't understand i how to prove my favorite group lemma :D Can anyone help me ?
example(G : Type)[group G] :((∀ c : G, c = c⁻¹) → (∀ a b : G, ab = ba)):=
begin
intro h,
intros a b,
calc
ab = (ab)⁻¹ : h (a*b)
... = b⁻¹ *a⁻¹ : by rw mul_inv_rev
... = b*a⁻¹ : sorry
... = b*a : sorry
end

You probably want to rewrite in the reverse direction, which can be accomplished by, e.g. rw ← h (where h is your equality hypothesis)

[Donald Sebastian Leung]

Also, you'd probably want to format your code next time, just so that it's a bit easier on the eyes of the person trying to help you

[Jason KY.]

I was able to solve it this way

variables {G : Type*} [group G]

example (y z : G) (h : ∀ x : G, x = x⁻¹) : y * z = z * y :=
begin
  suffices : z * y = z⁻¹ * y⁻¹,
    rw [this, h (y * z)], apply mul_inv_rev,
  conv {to_lhs, rw [h z, h y]}
end

[orlando cau]

Thx, i'm verry beginner, i try to understand your code !

[Donald Sebastian Leung]

By the way, did you try out the natural number game?

[orlando cau]

No i don't try natural number game ! I just see this tutorial and i try to understand the language ! thx

[Donald Sebastian Leung]

Nice :+1: Are you stepping through the tutorial in a web editor / VSCode, or are you just reading through the file on GitHub?

[orlando cau]

Ohhh it's Ok ! It's My first proof :grinning_face_with_smiling_eyes:

I install vs Code and lean yesterday !

variables {G : Type*} [group G]
example (a b : G) (h : ∀ x : G, x = x⁻¹) : a * b = b * a :=
begin
    calc
        a*b = (a*b)⁻¹  : by rw  ← h(a*b)
        ... = b⁻¹ *a⁻¹ : by rw mul_inv_rev
        ... = b*a⁻¹    : by rw ← h(b)
        ... = b*a      : by rw ← h(a)
end

[Kevin Buzzard]

variables {G : Type*} [group G]
example (a b : G) (h : ∀ x : G, x = x⁻¹) : a * b = b * a :=
calc
        a * b = (a * b)⁻¹ : by rw  ← h (a * b)
        ...   = b⁻¹ * a⁻¹ : by rw mul_inv_rev
        ...   = b * a⁻¹   : by rw ← h b
        ...   = b * a     : by rw ← h a

You don't need the brackets for h(a) etc -- in functional programming we know that h is a function so the next thing will be the input, we don't need brackets to tell us this. On the other hand the computer scientists like their spaces before and after *

[orlando cau]

Thanks Kevin, i try to do other little proof ! This is very fun !

[Kevin Buzzard]

But of course this is cheating, because you didn't prove mul_inv_rev :-)

[Kevin Buzzard]

Give me 1 minute and I will make you ten more questions like this.

[Kevin Buzzard]

Here -- you can build group theory from the axioms at this link

[Kevin Buzzard]

Start reading at line 50

[Kevin Buzzard]

@orlando cau

[orlando cau]

ok thank you i try this game :)

[orlando]

Hello Sorry, i got a problem with my computer :-( I don't do my homework !

[orlando]

Hello,

I read some tutorial and i do some exercice : but i have basic problem !

variables {G : Type} [group G]
def multiplication (a b : G) := a*b
def left_mul_by (a  : G) := λ b : G, multiplication a b
lemma test (a b c: G) (h : a = b) : c* a = c * b :=   ---- i try a first lemma because i don't understand the logic of the language
begin
    let f := left_mul_by c,
    show c * a = c * b, from eq.subst h f,          ---- don't work  :(
end

[Patrick Massot]

You don't need those definitions, and the proof is rw h.

[Patrick Massot]

What have you read so far?

[Patrick Massot]

You can spend years playing with Lean without ever writing eq.subst, which is a very low-level thing not intended for end-users.

[orlando]

ohhh, it's work ... thank you ! I read (a little) [this course] (https://leanprover.github.io/logic_and_proof/) and do some exercice !

[Patrick Massot]

How did you install lean+mathlib?

[Patrick Massot]

Do you have a working python+pip setup?

[orlando]

Yes i install lean + mathlib ! All it's ok !

[Patrick Massot]

Can you run pip install --upgrade mathlib-tools (maybe prefixed with sudo, and maybe replacing pip by pip3 depending on your python setup)?

[Patrick Massot]

If this work you can run

leanproject get tutorials
code tutorials

and read the file src/first_proofs.lean.

[Patrick Massot]

You can also play the natural numbers game online.

[orlando]

Hum it's does'nt work : but i'm on windows 10 ! Thx for the tutorial with real number it's very insteresting !

$ pip install --upgrade mathlib-tools
ERROR: Could not find a version that satisfies the requirement mathlib-tools (from versions: none)
ERROR: No matching distribution found for mathlib-tools

orlando@LAPTOP-487KLHV8 MINGW64 ~/my_project (lean-3.6.1)
$ pip3 install --upgrade mathlib-tools
ERROR: Could not find a version that satisfies the requirement mathlib-tools (from versions: none)
ERROR: No matching distribution found for mathlib-tools

[Patrick Massot]

What is your python3 version ?

[Patrick Massot]

Run python3 --version

[Patrick Massot]

And also "pip3 --version" for good measure

[orlando]

-- > Python 3.8.2
and
---> pip 20.0.2

[Patrick Massot]

Oops, it's my fault. I should have written: pip3 install mathlibtools (without the hyphen)

[orlando]

ok, no problem Patrick

[Patrick Massot]

I wish the pip error message could be more explicit. The current message makes it very hard to distinguish actual version issues with stupid typos.

[Patrick Massot]

@orlando does it work now?

[orlando]

it's ok i have the tuto !

[Patrick Massot]

Good, I hope you'll learn a couple of things by reading it.

[orlando]

thx you Patrick !

[orlando]

Hello @Kevin Buzzard i do your group game, but i have some problem :
1/ it's complicated !
2/ i don't finish ! (2 goals) !
3/ can i simplify ???
But : this is cooooooooool :sunglasses: thank you for this exercice !
groupe.lean

[Kevin Buzzard]

It's easier to read if you post the file directly like this:

import tactic
/-!
Basic definitions in group theory.
The beginner mathematician should ignore this part; definitions are
can be intimidating. Skip down to line 50, this part is technical.
-/

set_option old_structure_cmd true -- it's better for this kind of stuff

-- We're overwriting inbuilt group theory here so we always work in
-- a namespace

namespace mygroup

-- definitions of the group classes

section groupdefs

-- Set up notation typeclass using `extends`.
class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

-- definition of the group structure
class group (G : Type) extends has_group_notation G :=
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

class comm_group (G : Type) extends group G :=
(mul_comm : ∀ a b : G, a * b = b * a)

-- definition of powers
@[simp] def group_pow_nat {G : Type} [group G] : G → ℕ → G
| g 0 := 1
| g (n + 1) := group_pow_nat g n * g

instance group_has_pow_nat {G : Type} [group G] : has_pow G ℕ := ⟨group_pow_nat⟩

@[simp] def group_pow {G : Type} [group G] : G → ℤ → G
| g (int.of_nat n) := group_pow_nat g n
| g -[1+ n] := (group_pow_nat g (n + 1))⁻¹

instance group_has_pow {G : Type} [group G] : has_pow G ℤ := ⟨group_pow⟩

-- Center of a group
def center (G : Type) [group G] := {g : G | ∀ k : G, k * g = g * k}
attribute [reducible] center

@[simp] lemma mul_left_inv_simp{G : Type}[group G](a : G) : a⁻¹ * a = 1 :=
begin
    exact group.mul_left_inv a,
end
lemma rev_o {G : Type}[group G](a : G) : 1 = a⁻¹ * a  :=
begin
    exact eq.symm( group.mul_left_inv a),
end
@[simp] lemma mul_assoc_simp{G : Type}[group G](a b c : G) : a * b * c = a *(b * c ) :=
begin
    exact group.mul_assoc a b c,
end

@[simp] lemma rev_mul_assoc_simp{G : Type}[group G](a b c : G) :   a * (b * c ) = a * b * c :=
begin
    exact eq.symm (group.mul_assoc a b c),
end

end groupdefs

-- START HERE

/-

For a group G, you start with the following axioms:

mul_assoc : ∀ (a b c : G), (a * b) * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1

The goal is to prove the following theorems (in the order listed) :

`mul_left_cancel : ∀ (a b c : G), a * b = a * c → b = c`
`mul_eq_of_eq_inv_mul {a x y : G} : x = a⁻¹ * y → a * x = y`
`mul_one (a : G) : a * 1 = a`
`mul_right_inv (a : G) : a * a⁻¹ = 1`
`eq_mul_inv_of_mul_eq {a b c : G} (h : a * c = b) : a = b * c⁻¹`
`mul_left_eq_self {a b : G} : a * b = b ↔ a = 1`
`eq_inv_of_mul_eq_one {a b : G} (h : a * b = 1) : a = b⁻¹`
`inv_inv (a : G) : a ⁻¹ ⁻¹ = a`
`inv_eq_of_mul_eq_one {a b : G} (h : a * b = 1) : a⁻¹ = b`
`mul_inv_rev {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹`

-/

variables {G : Type} [group G]
variables (x y z : G)
lemma trans_appl(f : G → G) : ∀ a b : G, a = b → f a = f b :=
begin
    intros a b,
    intro h,
    exact congr_arg (f) h
end
lemma mul_left_cancel (a x y : G) :  a * x = a * y  →  x = y :=
begin
    intro h,
    let p := a*x,
    let q := a*y,
    have h1 : p = q, from h,
    have hp : (a⁻¹ * a) * x = 1 * x, from  trans_appl (λ t : G, t *x) (a⁻¹ * a) (1) (mul_left_inv_simp a),
    have hq : (a⁻¹ * a) * y = 1 * y, from  trans_appl (λ t : G, t *y) (a⁻¹ * a) (1) (mul_left_inv_simp a),
    have Hpq : a⁻¹ * (a *x) = a⁻¹ * (a*y), from trans_appl (λ t : G, a⁻¹ *t) (a *x)  (a*y) h,
    calc
        x   = 1 * x            : eq.symm (group.one_mul x)
        ... = a⁻¹ * a * x      : eq.symm (hp)
        ... = a⁻¹ * (a *x )    : group.mul_assoc a⁻¹  a x
        ... = a⁻¹ * (a*y)      : Hpq
        ... = a⁻¹ * a*y        : rev_mul_assoc_simp (a⁻¹)  a y
        ... = 1 * y            : hq
        ... =  y               : group.one_mul y
end

lemma mul_eq_of_eq_inv_mul {a x y : G} (h : x = a⁻¹ * y) : a * x = y :=
begin
---  Strategie :
---                  x = a⁻¹ y  =>  a^⁻¹ a x = a⁻¹ y  and use lemma mul_left_cancel a^⁻¹ ax y to get ax = y
---
    have hx : (a⁻¹ * a) * x =1 *  x, from trans_appl (λ t : G, t *x) (a⁻¹ * a) (1) (mul_left_inv_simp a),
    have h1 : 1 * x   = x, from group.one_mul x,
    have H : (a⁻¹ * a) * x = a⁻¹ *y, from calc
        (a⁻¹ * a) * x = 1 * x : hx
        ...           = x     : h1
        ...           = a⁻¹ *y : h,
    have G : a⁻¹ * (a *x) = a⁻¹ *y, from calc
        a⁻¹ * (a *x) = (a⁻¹ * a) * x : rev_mul_assoc_simp a⁻¹  a x
        ...          = a⁻¹ *y        : H,
    show a * x = y, from mul_left_cancel (a⁻¹) (a*x) (y) (G),
end

theorem mul_one (a : G) : a * 1 = a :=
begin
  have H : 1 = a⁻¹ * a, by simp,
  show a * 1 = a, from mul_eq_of_eq_inv_mul (H),
end

theorem mul_right_inv (a : G) : a * a⁻¹ = 1 :=
begin
  have h : a⁻¹ = a ⁻¹ *1, from eq.symm (mul_one a⁻¹),
  show a *a⁻¹ = 1, from mul_eq_of_eq_inv_mul (h),
end

lemma eq_mul_inv_of_mul_eq {a b c : G} (h : a * c = b) : a = b * c⁻¹ :=
begin
    have H : ( a *  c ) * c⁻¹  = b * c ⁻¹,
        from  trans_appl (λ t : G, t *c⁻¹ ) (a * c) (b) (h),
    show  a = b * c⁻¹ , from calc
        a       = a * 1             :  eq.symm (mul_one (a))
        ...     = a * (c * c⁻¹ )    :  trans_appl(λ t : G, a * t) (1) (c * c⁻¹) (eq.symm (mul_right_inv c))
        ...     = ( a *  c ) * c⁻¹  :  rev_mul_assoc_simp (a) (c) (c⁻¹)
        ...     = b * c⁻¹           : H
end
lemma mul_left_eq_self {a b : G} : a * b = b ↔ a = 1 :=
begin
    sorry --- i dont know iff.intro ? ? ? or Split ??? i don't understand !
end

lemma eq_inv_of_mul_eq_one {a b : G} (h : a * b = 1) : a = b⁻¹ :=
begin
  have H : a = 1 * b⁻¹, from eq_mul_inv_of_mul_eq (h),
  show a = b⁻¹, from calc
    a   = 1 * b⁻¹  : H
    ... = b⁻¹      : group.one_mul (b⁻¹),
end

lemma inv_inv (a : G) : a ⁻¹ ⁻¹ = a :=
begin
  let b := a⁻¹,
  have h : a * b = 1, from mul_right_inv a,
  show b⁻¹ = a, from eq.symm (eq_inv_of_mul_eq_one h),
end

lemma inv_eq_of_mul_eq_one {a b : G} (h : a * b = 1) : a⁻¹ = b :=
begin
  have H : a = b⁻¹, from eq_inv_of_mul_eq_one h,
  have He:  b = a⁻¹ , from calc
        b       = b⁻¹ ⁻¹  : eq.symm(inv_inv b)
        ...     = a⁻¹     : trans_appl(λ t : G, t⁻¹ ) (b⁻¹ ) (a) (eq.symm H),
    show a⁻¹ = b, from eq.symm He,
end

-- for orlando cau
lemma mul_inv_rev {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  sorry
end
end mygroup

[Kevin Buzzard]

For the iff you can start like this:

begin
  split,
  { intro h,
     ...
  },
  { intro h,
     ...
  },
end

[Kevin Buzzard]

the other goal is the one you need for your favourite lemma :-) Why not start with apply inv_eq_of_mul_eq_one?

I am just racing out the office, certainly your proofs can be simplified but it's pretty cool that you did so many :-)

[orlando]

@Kevin Buzzard thx for the split iff ! For my favorite lemma, yes is the one :grinning: i have the maths proof but it's complicated to do !
I will make it : Probably tomorrow !

[Kevin Buzzard]

What's the maths proof?

[orlando]

(a * b) (b⁻¹ * a⁻¹) = 1 so by  inv_eq_of_mul_eq_one : (a * b)⁻¹ = b⁻¹ * a ⁻¹

[Kevin Buzzard]

So why not apply inv_eq_of_mul_eq_one?

[Kevin Buzzard]

Computer scientists like to write proofs backwards

[Patrick Massot]

You don't have to go backwards, nothing prevents you to write:

 have key : (a * b)*(b⁻¹ * a⁻¹) = 1,
  sorry,
 exact  inv_eq_of_mul_eq_one key,

[Patrick Massot]

and replace sorry by a proof of course.

[orlando]

Yes i do that ! But the proof is a little complicated :rolling_on_the_floor_laughing:

lemma mul_inv_rev {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
    have H : b * b⁻¹ *a⁻¹ = 1 *a⁻¹,
            from trans_appl(λ t : G, t * a⁻¹ ) (b *b⁻¹) (1) (mul_right_inv b),
    have Ha : b * (b⁻¹ *a⁻¹) = a⁻¹, from calc
        b * (b⁻¹ *a⁻¹) = b * b⁻¹ *a⁻¹ : rev_mul_assoc_simp (b) (b⁻¹) (a⁻¹)
        ...          = 1 *a⁻¹    : H
        ...          = a⁻¹       : group.one_mul a⁻¹,
    have h : (a * b) * (b⁻¹ * a⁻¹)= 1, from calc
        (a * b) * (b⁻¹ * a⁻¹)  = a * (b * (b⁻¹ * a⁻¹)) : mul_assoc_simp (a) (b) (b⁻¹ * a⁻¹)
        ...                    = a * a⁻¹             : trans_appl(λ t : G, a*t ) (b * (b⁻¹ * a⁻¹)) (a⁻¹) (Ha)
        ...                    = 1                   : mul_right_inv a,
    exact inv_eq_of_mul_eq_one (h),
end

[Kevin Buzzard]

Why not just apply and then rewrite a couple of times?

[Kevin Buzzard]

These systems are designed to go backwards

[orlando]

i don't know, how can i do that :D

[Kevin Buzzard]

Did you do the apply line yet?

[orlando]

what is the apply line ? (sorry i'm not english, i'm French and don't speack very well)

[Mario Carneiro]

Kevin Buzzard said:

So why not apply inv_eq_of_mul_eq_one?

add this to your proof

[Kevin Buzzard]

and then start rewriting, e.g. rw mul_assoc

[Kevin Buzzard]

actually the rewrites are problematic because they clash with the real definitions in the root namespace. Change the end of your file to this:

namespace group

-- for orlando cau
lemma mul_inv_rev {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply inv_eq_of_mul_eq_one,
  rw mul_assoc,
  sorry
end

end group

end mygroup

[Kevin Buzzard]

That namespace group line could really do with being on the line before -- START HERE

[orlando]

okay !!!!

lemma mul_inv_rev' {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply inv_eq_of_mul_eq_one,
  rw mul_assoc_simp,
  apply mul_left_cancel a⁻¹ ,
  rw rev_mul_assoc_simp,
  rw mul_left_inv,
  rw one_mul,
  rw rev_mul_assoc_simp,
  rw mul_one,
  rw mul_right_inv,
  rw one_mul,
end

[Patrick Massot]

You don't have to use apply if you don't want it, and you don't have to make it complicated. You can write:

lemma mul_inv_rev {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
 have key : (a * b)*(b⁻¹ * a⁻¹) = 1,
  rw [group.mul_assoc, ← group.mul_assoc b, mul_right_inv, group.one_mul, mul_right_inv],
 exact  inv_eq_of_mul_eq_one key,
end

[Patrick Massot]

If you want the proof script to be readable, you can use a calc to do the exact same proof:

example {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
 have key :=
 calc (a * b)*(b⁻¹ * a⁻¹)
        = a*(b*(b⁻¹*a⁻¹)) : by rw group.mul_assoc
    ... = a*(b*b⁻¹*a⁻¹)   : by rw ← group.mul_assoc b
    ... = a*(1*a⁻¹)       : by rw mul_right_inv
    ... = a*a⁻¹           : by rw group.one_mul
    ... = 1               : by rw mul_right_inv,
 exact  inv_eq_of_mul_eq_one key,
end

[Patrick Massot]

But really the last three lines (at least) shouldn't be there. The problem is that your file completely messes up simp attribute (that are tricky to use right). You need to remove them from the associativity lemmas, and add them to mul_left_inv, mul_right_inv, one_mul and mul_one. Then you can write:

example {a b : G} : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
 have key : (a * b)*(b⁻¹ * a⁻¹) = 1,
  rw [group.mul_assoc, ← group.mul_assoc b],
  simp,
 exact  inv_eq_of_mul_eq_one key,
end

[Patrick Massot]

The actual nice proof would of course be entirely automatic. Currently I think even mathlib cannot do it fully automatically, but this is only a matter of finding someone who knows a bit of tactic writing and has time for it...

[Patrick Massot]

orlando said:

what is the apply line ? (sorry i'm not english, i'm French and don't speack very well)

I guessed that from your Lean file name :wink: Where are you? (sorry if you already answered that question, there too many new users for me to remember everyone).

[Mario Carneiro]

I guessed it from the space before the question mark

[Patrick Massot]

In my case you even get more information from that: I have spaces before question marks when I'm typing on my phone, because I'm too lazy to switch to English keyboard or go back and erase spaces introduced automatically.

[Johan Commelin]

Il y a beaucoup de Français ici. :wink:

[Johan Commelin]

(But I'm not one of them... although I live 8km from the border...)

[orlando]

@Patrick Massot thank you, for the comment ! It's nice, i will try to simplify my proof with rw, it's a good exercice for me, i want to understand :grinning:

Bonjour de la France (Grenoble Alpes) @Johan Commelin

[orlando]

Hello,

I have a problem :innocent:

variables (R : Type) [comm_ring R]
def Gm  :=  { x : R | ∃ y : R, x * y = 1 }
example (a b : R) : (a ∈  Gm(R)) → (b ∈ Gm(R)) →  (a * b ∈  Gm(R)) :=
begin
    intros ha hb,
    unfold Gm at ha,
    sorry  -- a ∈ Gm(R) so exist y_a s.t a * y_a = 1, how to have y_a
           -- ellim.exist  doesn't work directly ?
end

[Johan Commelin]

cases ha with y hy

[Johan Commelin]

Alternatively, replace your intros with rintros?, and see what it tells you.

[orlando]

Cases is ok ... thank you :slight_smile:
I will try to make Gm a group :tada:

[Kevin Buzzard]

Then you could make Gm a group functor

[Patrick Massot]

Orlando, you can still pick up the efficient way from the beginning: the first line of this proof should be rintros ⟨a', ha⟩ ⟨b', hb⟩,

[orlando]

Ok, verry nice Patrick !!!

Kevin, yes it's my goal, but slowly, i have to study the language before !

[Kevin Buzzard]

I guess it's worth saying that Gm is already defined in lean and it's called units. But feel free to define it yourself for practice

[Kevin Buzzard]

You can look at how it was done in mathlib after

[orlando]

@Kevin Buzzard

I learn a little about units and i make my favorite commutative algebra lemma, it's fun but complicated ! it's killing me :sweat_smile:

---
---   Goal : 0. Understand with a little example :D
---             create  Gm : R → Ab has a group fonctor from category of ring → Abelian group
---           -----------------------  > > > > >   difficult !    I have to make a group first :D

import tactic.ring
universe u
variable {R : Type u}
structure Gm (R : Type u) [comm_ring R] :=   --- Object ?
(val : R)
(inv : R)
(val_inv : val * inv = 1)
(inv_val : inv * val = 1)
namespace Gm
variables [comm_ring R]
------    My universe
instance : has_coe (Gm R) R := ⟨val⟩    ---- ici c'est la valeur de l'unité dans R instance ???
--- Exemple of Gm element !
def Nil_lemma_for_fun___D(a : R) : (a * a = (0 : R)) → Gm R :=
    begin
        --- My favorite commutative lemma : η^2 =0 → (1+η) × (1-η) = 1 so 1+η ∈ Gm(R) :D
        ---                               :
        intro h,
        let val_inv : (1+a)* (1-a) = 1, from
            calc
                (1+a) * (1-a) = 1*1  - a*a        : by rw [eq.symm (mul_self_sub_mul_self_eq (1) (a))]
                ...           = 1*1  - 0          : by exact congr_arg (λ l, 1*1 - l)  (h)
                ...           = 1                 : by simp,
        let inv_val : (1-a)* (1+a)= 1, from
            calc
                (1-a) * (1+a) = (1+a) * (1-a)    : by rw mul_comm
                ...          = 1                 : val_inv,
        exact ⟨1+a,1-a, val_inv,inv_val⟩
    end

protected def  linv (x : Gm R) : (Gm R) := ⟨x.inv,x.val,x.inv_val,x.val_inv⟩
--- Perhaps i can drop inv_val cause commutativity (all Ring are commutative :D)
/-- Gm herite de la structure de la multiplication de R -/
protected def mul (u₁ u₂ : Gm R) : Gm R :=
⟨u₁.val * u₂.val,
u₂.inv * u₁.inv,
have u₁.val * (u₂.val * u₂.inv) * u₁.inv = 1, by
begin
    let a  := u₁.val,
    let b  := u₂.val,
    let b' := u₂.inv,
    let a' := u₁.inv,
    show  a * (b * b') * a' = 1, from
        calc
            a * ( b * b' ) * a' =  (a * 1) * a'     : by exact congr_arg (λ l, a * l  * a')  (u₂.val_inv)
            ...                 =   a * a'          : by rw mul_one a
            ...                 =   1               : by rw u₁.val_inv,
end,
by simpa only [mul_assoc],
have u₂.inv * (u₁.inv *u₁.val) * u₂.val  = 1, by
begin
    let b'  := u₁.val,
    let a'  := u₂.val,
    let a   := u₂.inv,
    let b   := u₁.inv,
    show  a * (b * b') * a' = 1, from
        calc
            a * ( b * b' ) * a' =  (a * 1) * a'     : by exact congr_arg (λ l, a * l  * a')  (u₁.inv_val)
            ...                 =   a * a'          : by rw mul_one a
            ...                 =   1               : by rw u₂.inv_val,
end,
by simpa only [mul_assoc],  -- what is simpa  = Sympathique ???
⟩
instance : has_mul (Gm R) := ⟨Gm.mul⟩
instance : has_one (Gm R) := ⟨⟨1, 1, mul_one 1, one_mul 1⟩⟩
instance : has_inv (Gm R) := ⟨Gm.linv⟩
end Gm

[Yury G. Kudryashov]

There are many facts about units in algebra/group/units.

[Yury G. Kudryashov]

They're defined in any (incl. non-commutative) monoid, but you can think about a ring, if you want.

[orlando]

Hello @Yury G. Kudryashov

Okay, but i want learn how to use, so i redo some stuff :grinning_face_with_smiling_eyes: it's difficult for a beginner to learn !

[Yury G. Kudryashov]

simpa is more or less simp; assumption, and simpa using lalala is something like have this := lalala; simp at this |-; assumption

[orlando]

Hello,

I have i little problem with the existential quantifier :upside_down:

import tactic.ring
import tactic.ring_exp
import algebra.ring
universes u           ---- ???
variables {R_1 : Type u}{R_2 : Type u}[comm_ring R_1][comm_ring R_2]
structure Idem(R : Type u)[comm_ring R] :=
(e : R)(idem : e*e  = e)
namespace Idem
def map( f : ring_hom R_1 R_2) : Idem (R_1) → Idem R_2  :=
 λ E, ⟨ f E.e, by rw  [← f.map_mul, E.idem]⟩
end Idem

structure Uni_2(R : Type u)[comm_ring R]  :=
(a : R)
(b : R)
(certificat : ∃ x y : R, a * x + b * y = (1 : R))
namespace Uni_2
def map( f : ring_hom R_1 R_2) : Uni_2 R_1 → Uni_2 R_2  :=
 λ ob, ⟨ f ob.a,f ob.b,  begin
        cases ob.certificat with xob h,      -- how to get directly xob and yob ? with one cases ?
        cases h with yob n,
        have H : (f ob.a) * (f xob) +  (f ob.b) * (f yob) = 1, by
        rw  [← f.map_mul,← f.map_mul,← f.map_add,n,f.map_one]
        ,sorry,
        end,
        ---          I dont understand how to use (f xob) (f yo),  i have the certicate H   :(
        ⟩
end Uni_2

[Kevin Buzzard]

        use f xob,
        use f yob,
        assumption,

[Kevin Buzzard]

hey, you've come a long way recently :-)

[Kevin Buzzard]

The universes u thing is because this is not ZFC, they are assuming the existence of infinitely many inaccessible cardinals shrug. It means that category theory is easier because you don't have to keep fussing about the difference between sets and classes, but I have never really seen the point of it. You are supposed to be even more universe polymorphic and write universes u v and {R_1 : Type u}{R_2 : Type v}. But if you don't put the line at all and just write {R_1 : Type}{R_2 : Type} it works fine.

[Kevin Buzzard]

rcases ob.certificat with ⟨xob, yob, n⟩, is how to get everything directly.

[orlando]

you're a magician @Kevin Buzzard !!!

Ps : i will try to contruct some action of Gm on Uni_2 :-D

[orlando]

@Kevin Buzzard : okay for universes, an other question : what is the difference betwen $a \in R$ and a : R ?

[Kevin Buzzard]

Nothing really.

[Kevin Buzzard]

In set theory we say that a ring is a set R plus addition, multiplication, axioms. In type theory they say a ring is a type R plus addition, multiplication, axioms.

[Kevin Buzzard]

One difference is that in set theory, the elements of R are also sets, even though we have to remember never to ask about their elements because the elements are irrelevant. In type theory, the terms of type R are just terms, they are not types, and in particular we can't ask for their elements. If r : R then a : r doesn't make sense.

[Kevin Buzzard]

This the good part of type theory -- we think of R as a set and then we just forget that its elements are also sets, we treat them as "atoms". In type theory they really are atoms, so it is closer to how we think about things.

[Kevin Buzzard]

The bad part of type theory is that every term has exactly one type, so this means that the natural number 3, the integer 3, the real number 3 etc are all different 3's. The function $\mathbb{N}\to\mathbb{Z}$ is not the inclusion, it's the "coercion", and these functions are a bit annoying at first because mathematicians don't ever explicitly think about them and it takes a while to learn how to deal with them.

[orlando]

Ok, if a and b satisfy a b : R , you can form new type (a = b), in my example * Idem , 'Idem' is an example of this type !

[Kevin Buzzard]

Oh yeah that's the other use of types. There are two universes of types: Type and Prop. The terms of type Type are what mathematicians think of as sets -- e.g. the reals, the p-adic numbers, a group, a manifold, whatever. The terms of type Prop are true-false statements e.g. the Riemann Hypothesis, the statement 2+2=4 or the statement 2+2=5. If R : Type then x : R is what we call an element of R. If P : Prop then h : P is what we call a proof of P. So type theory can be used to unify these two ideas of sets and functions, and of true/false statements and implications. $P\implies Q$ is written P → Q in Lean and is thought of as a function from proofs of $P$ to proofs of $Q$, which is exactly what $P\implies Q$ gives you.

[Kevin Buzzard]

It's a crazy way to think about mathematics but now this is the way I think about it, and it is no different to the usual way really, it's just a different point of view.

[Kevin Buzzard]

A proof of ∀ n, 2 * n = n + n is a function which takes as input a number $n$, and then as output gives a proof of $2n=n+n$.

[Kevin Buzzard]

Everything is a function in this world.

[orlando]

1/ it's really an interesting point of view. In fact (i learn this in a video), a=b is the type of proof that a b, but if you have two proofs: p q: [a= b], you can form a new type [p=q] ect ! I have to think more about this but I have met several times examples where it is important to pay attention to the proof of equality (to the different proof)! (i use google traductor my english is bad!)

2/ the work you did on lean and mathlib is really execptional! Congratulations! It's a great project, I hope to understand a little more !

[Kevin Buzzard]

I did nothing on Lean and essentially nothing on mathlib. I absolutely agree it's exceptional.

That stuff about different proofs of a = b is not true in Lean. It is true in some other systems. In Lean there is at most one proof of a = b. This is a very big subject, but as a mathematician I find the whole thing ridiculous.

[Kevin Buzzard]

I use Lean because it seems that this design decision makes a system which is much better for the kind of mathematics which I do.

[Kevin Buzzard]

What is your background?

[Kevin Buzzard]

I'm an algebraic number theorist in London.

[Patrick Massot]

Orlando, you can also have a look at https://leanprover-community.github.io/lean-perfectoid-spaces/type_theory.html about foundations

[orlando]

I'm not an 'academic mathematician', I just wrote a thesis in the inverse Galois problem' in 2011. Now I study mathematics for my pleasure, I do not have a great theoretical background! But I know a bit of number theory and algebraic geometry (but really little, it's complicated).

[orlando]

thx @Patrick Massot

[orlando]

@Kevin Buzzard : I little arithmetic joke, i have no proof … key : Artin conductor, Serre-Deligne … too complicated for me :yum:

Let $f = \boxed{ \frac{E_6^5 +7 E_4^3 E_6^3-8 E_6E_4^6}{15552}}$ where $E_6$ and $E_4$ are Eisenstein series :

sage: E4
1 + 240*q + 2160*q^2 + 6720*q^3+...

I give you $f$ :

q - 99180*q^3 - 82300928*q^4 - 9240014250*q^5 - 250922631168*q^6 - 1803292256920*q^7 + 3927484661760*q^8 + 69888751712253*q^9 + 52730118144000*q^10 - 1073448094642308*q^11 - 2159808927252480*q^12 + 8077328528018750*q^13 + 30845089913831424*q^14 - 28190600602173000*q^15 - 203338491650637824*q^16 - 249926961314852910*q^17

Denote by $a_n$ the coefficient of $f$ and let $P = x^3 - 3x^2 + 11x - 17 \in \mathbb{\Z}[x]$.

We have : forall prime $p$ : $\boxed{ a_p = N_p-1 \pmod{59} }$ where $N_p$ is the Numbers of roots of $P$ in $\mathbb{F}_p$ !

Exemple : we have $a_{17} = - 249926961314852910 = 2 \pmod{59}$ so three root for $P \pmod{17}$ !

sage: g
x^3 - 3*x^2 + 11*x - 17
sage: p
17
sage: g.factor_mod(p)
x * (x + 5) * (x + 9)

Good night !

[Kevin Buzzard]

What you say isn't true for p=2 (the discriminant of the polynomial is a multiple of 2, even though the discriminant of the field it generates is not) and it may or may not be true for p=59 (one would have to do an explicit check). For all other primes $p$ one can argue as follows: the space of level 1 weight 30 cusp forms is 2-dimensional and the basis of eigenforms is a pair of Galois conjugate forms defined over $\mathbb{Q}(\sqrt{51349})$. One checks that $59$ splits in this field ($14^2$ is congruent to $51349$ mod $59$), so there are two mod 59 Galois representations attached to this form. With notation as in the LMFDB link, $\beta$ is $96\sqrt{51349}$ is congruent to $\pm46$ and setting $\beta=-46$ mod 59 shows that one 59 specialisation of the eigenform is precisely mod 59 reduction of the form you write down (the coefficients agree for $q^i$ for $i\leq2$ and this is enough). The splitting field of $P$ is unramified outside of 59 and has Galois group $S_3$, and your claim (for $p\not=2,59$) follows from the claim that the mod 59 Galois representation attached to the eigenform (corresponding to the $\mathfrak{p}$-adic place above $\mathbb{Q}(\sqrt{51349})$ where $\beta\equiv-46$) has image precisely $S_3$. Note that the $k-1=29$'th power of the mod 59 cyclotomic character is the quadratic character corresponding to the quadratic subfield of the splitting field of $P$ so all the numerics check out. The $S_3$ representation is modular, coming from a weight 1 cusp form, and some standard level and weight optimisation shows that there is a mod 59 representation of level 1 and weight 30 corresponding to the representation; it suffices to prove that this is our mod 59 eigenform, but it must be one of the two eigenforms so again you can check which one it is by writing down the power series to enough terms, and indeed you already did that. So done :-)

[orlando]

Ok, thx Kevin , for the prime $2$ (my bad), This is really crazy arithmetic :smiley: Yes i write down the series and do computation and also the trick $30 -1= \frac{59-1}{2}$ :innocent: But this is really deep mathematics !!! My example is just a baby-instance and i can't go further !

[orlando]

Hello,

i have 2 little question :

1. it's possible to create a functor from Ring to Ring ! that send $R$ to $R[X]$ ?

2. Is there a structure of commutative ring for $R[X]$ (in lean) Where $R$ is a commutative Ring ?

import tactic.ring
import data.polynomial
import algebra.category.CommRing.basic

open category_theory
open functor
open CommRing
open polynomial
universes  v u
local notation `Ring` := CommRing.{u}
local notation `Set` :=  Type u               -


def poly :  Ring  ⥤  Set :=
{ obj :=   λ α : Ring, polynomial α,
  map := λ( α β : Ring) (f : α ⟶ β),   polynomial.map f,
}

(deterministic) timeout

[Kevin Buzzard]

Lean does a lot of stuff without using the category theory language. The construction is called polynomial:

import data.polynomial

noncomputable example (R : Type) [comm_ring R] :
  comm_ring (polynomial R) := by apply_instance

The import gives you a function polynomial which eats a type and returns a new type. The example shows that if the type it eats is known by the typeclass system to have a ring structure, then the output type also gets a ring structure.

[orlando]

Thx Kevin,

i have to stop a couple a day, i will go back next week, have fun and thx again for all !

[orlando]

@Kevin Buzzard
I can't move cause @corona bidule !!!

So I try to explain my goal in the middle of the file ! (Hard computation for the moment, but i want to simplify all) !

import tactic.ring
import tactic.ring_exp
import algebra.category.CommRing.basic

open CommRing

universes v u
local notation ` Ring `     :=    CommRing.{u}
local notation ` Set  `     :=    Type u

---          study of co-maximal familly ! I do the job why two elements for the moment  !
namespace co_maxi
variables (R : Type u) [comm_ring.{u} R ]

def co_max  (a b : R) : Prop   :=
             ∃ u v :  R,    a * u + b * v = 1

local infix     ⊥  :=  co_max R   --- notation

lemma one_perp (a : R)    :  1 ⊥ a :=   --- with 1 * 1 + a * 0 = 1
begin
    have h: 1 * 1 + a * 0 = 1,
        rw [one_mul,mul_zero,add_zero],
    use ⟨1,0,h⟩
end

lemma symm (a b : R) : (a ⊥ b) →  (b ⊥ a)  :=   --- a u + b v = 1 → b v + a u = 1
    λ ⟨u,v,k⟩,
        begin
            have  t :  b * v + a * u = 1,
                rw add_comm,  assumption,
            use ⟨v,u,t⟩,
        end

lemma abab_trick (a b c : R) : (a ⊥ c) → (b ⊥ c) → (a * b) ⊥ c :=    ---  Trick to simplify proof !  if a ⊥ c and b ⊥ c then ab ⊥ c  from calculus !
    λ ⟨ua,va,ka⟩  ⟨ub,vb,kb⟩,
        begin
            have J : (a * b) * ( ua * ub) + c * ( a * ua * vb + va * b * ub + va * c * vb) = 1,
                 by calc
                    (a * b) * ( ua * ub) + c * ( a * ua * vb + va * b * ub + va * c * vb)  =  (a * ua + c * va) * (b * ub + c * vb) : by ring_exp
                    ...                                                                    =   1                                    : by rw [ka,kb, one_mul],
        use ⟨ ua * ub,  a * ua * vb + va * b * ub + va * c * vb , J⟩,
        end
---- We do the big calculus, now is trivial induction !
---- for exemple a ⊥ c →  a^2 ⊥ c  using abab_trick a a c !  induction ...
open nat
lemma star (a  b : R) (n : nat):   (a ⊥ b) → ((a^n) ⊥ b)  :=
    λ u,
        nat.rec_on n
                (show  (a^0) ⊥ b, {rw pow_zero a, apply one_perp, })
                (assume n, assume re : ((a^n) ⊥ b), show (a^(n+1)) ⊥ b,
                       {rw pow_succ a n,apply abab_trick, assumption,assumption})

theorem My_favorite_localisation_lemma (a b : R) (n m : nat) : (a ⊥ b) → (a^n) ⊥ (b^m) :=                 --- the goals
    λ u, begin
        apply star,
        apply symm,    -- is there a repeat method ? How to programme such method ?
        apply star,
        apply symm,
        assumption,
    end
----
---     We want to proof 𝔸 is a local functor : a scheaf for global Zariski for Affᵒᵖ.
----   ( Note 𝔸 is structural for Ring so if you do the job for 𝔸 you do the job for all ring i.e Spec R := Hom(R,•) is a scheme (in sense of functorial geometry)
---    (ref Jantzen : 'algebraic group and representation' the first chapter) for all ring R : i can explain) !
---                 for the moment only with 2-covering famillies
---     There is two axioms :
---             1/ Separation : (for two elements ONLY)
---                      let R : comm_ring
---                      Let f,g ∈ R :  f ⊥ g.
---                      Let a ∈ R :
---                             ∃ m n : ℕ,  f^m a = 0 ∧  g^n a = 0   --- i.e a = 0 in localisation  {f^k k ∈ N⋆} and   {g^k k ∈ N⋆}
---                      Since f ⊥ g , we have f^m ⊥ b^n
---                      Have (u,v) s.t   f^m u + g^n v = 1
---                      multipliying by a give f^m au  + g^n a v = a  so 0 = a !
---    Note : i don't use Localisation library for the moment (i have to study) !
theorem Separation_axiom (a : R) (f g : R) : f ⊥ g → ( ∃ m n : ℕ, f^m * a = 0 ∧ g^n * a = 0 )   →   a = 0  :=  λ certif  ⟨m,n,proof⟩,
begin
    have H : (f^m) ⊥ (g^n),
        apply My_favorite_localisation_lemma,
        assumption,
    rcases H with ⟨ua,va,ka⟩,
        apply eq.symm,
        have H :  0  = (f ^ m * a* ua  +  g ^ n *a * va),
            rw [proof.1,proof.2],
            apply eq.symm,
            rw [zero_mul,zero_mul,add_zero],
        have G : (f ^ m * a* ua  +  g ^ n *a * va) = (f ^ m * ua  +  g ^ n  * va) * a,
        ring,
        rewrite [H,G,ka,one_mul a],
end
---   Gluing_axiome :
---
set_option class.instance_max_depth 20
theorem gluing_data (f g : R)(s_f s_g : R) (n : ℕ) :
         f ⊥ g → (∃ m : ℕ, f^m * g^(n+m) * s_f = g^m * f^(n+m) * s_g) →  (∃ s : R, ∃ N_f N_g : ℕ, f^(N_f+n) * s = f^N_f * s_f ∧  g^(N_g+n) * s = g^N_g * s_g) :=
         λ certif ⟨m,proof_m⟩, begin
            have H: (f^(n+m)) ⊥ (g^(n+m)),
                apply My_favorite_localisation_lemma,
                assumption,
            rcases H with ⟨vf,vg,proof_n_plus_m_f_g⟩,
            existsi [vf *s_f * f^m+ vg*s_g*g^m,m,m],
                split,
                    have H : f ^ (m + n) * (vf * s_f * f ^ m + vg * s_g * g ^ m) =   ( f ^ (n + m)* vf * s_f * f ^ m +  g ^ m *f ^ (n + m) *s_g * vg),
                        ring_exp,
                        rw [H,eq.symm proof_m],
                            have B : f ^ (n + m) * vf * s_f * f ^ m + f ^ m * g ^ (n + m) * s_f * vg = f^m *s_f *(f ^ (n + m) * vf + g ^ (n + m) * vg),
                            ring,
                            rw [B,proof_n_plus_m_f_g,mul_one],
                    have H : g ^ (m + n) * (vf * s_f * f ^ m + vg * s_g * g ^ m) =      f ^ m *g ^ (n+m) *s_f *vf + g ^ m* g ^ (n + m) * vg * s_g,
                        ring_exp,
                    rw [H,proof_m],
                        have B : g ^ m * f ^ (n + m) * s_g * vf + g ^ m * g ^ (n + m) * vg * s_g = g^m * s_g *(f ^ (n + m) * vf + g ^ (n + m) * vg ),
                        ring,
                        rw [B,proof_n_plus_m_f_g,mul_one],
end

[Kevin Buzzard]

        repeat {apply star, apply symm},    -- is there a repeat method ? How to programme such method ?
        assumption,

[Kevin Buzzard]

and end with end co_maxi and you're done. I don't understand what your question is.

[orlando]

Hello,

My question is, do you have an idea to simplify calculus, i have to do the same thing for a familly $(f_1,\dots,f_n)$ of comaximal element of a ring. It's complicate computation ! For the moment, i have no idea how to do that ! Perhaps the library "localization " can help !

[Kevin Buzzard]

My MSc student Ramon Fernandez Mir did this here.

[Kevin Buzzard]

There is an interesting story behind it all, but nobody wrote the paper yet. Here is Ramon's write-up.

[Patrick Massot]

You can compress stuff a bit when it's trivial, for instance the beginning could be:

lemma one_perp (a : R)    :  1 ⊥ a :=   --- with 1 * 1 + a * 0 = 1
⟨1,0, by ring⟩

lemma symm (a b : R) : (a ⊥ b) →  (b ⊥ a)  :=   --- a u + b v = 1 → b v + a u = 1
λ ⟨u,v,k⟩, ⟨v,u, by rwa add_comm⟩

lemma abab_trick (a b c : R) : (a ⊥ c) → (b ⊥ c) → (a * b) ⊥ c :=    ---  Trick to simplify proof !  if a ⊥ c and b ⊥ c then ab ⊥ c  from calculus !
    λ ⟨ua,va,ka⟩  ⟨ub,vb,kb⟩,
        begin
            have J := calc
                    (a * b) * ( ua * ub) + c * ( a * ua * vb + va * b * ub + va * c * vb)  =  (a * ua + c * va) * (b * ub + c * vb) : by ring
                    ...                                                                    =   1                                    : by rw [ka,kb, one_mul],
        use ⟨ ua * ub,  a * ua * vb + va * b * ub + va * c * vb , J⟩,
        end

[Kevin Buzzard]

I remember Mario once saying that it didn't matter if the proof looked incomprehensible if the statement was mathematically trivial, because then nobody wants to read the proof anyway.

[Patrick Massot]

I don't even think those proofs are less readable than the original ones.

[orlando]

Hum i try to read (to understand the language) some proof and it's very difficult ! Patrick thx you !

Perhaps a stupid question (sorry) : i thinck i don't understand something ?

import ring_theory.algebra
import data.polynomial
import data.finsupp
import data.zmod.basic
import tactic.ring
import algebra.category.CommRing.basic
import foncteur.comax
open zmod
@[reducible] def R : Type := zmod(15)
def  eval  : ℤ  → R :=
    λ n, n
#eval eval(19)
open co_maxi
def A :=   co_maxi.gluing_data R (6)(-5) 1 (-1) 1 ⟨ 1,1, by ring⟩  ⟨1,by ring ⟩  ---  6 * 1 + (-5) *1 = 1,  ,m = 1 cause  6 × 5 = 0
--- The gluing point is 4 because 4 mod 3 = 1 and 4 mod 5 = -1,
#print A --- where is 4 ???
-- Can I execute my proof ?? or it's a stupid idea ? -- i give Lean all the calculus so he have the answer ! ! ! But where ???

[orlando]

import fonctor.comax is my previous file !

[Kevin Buzzard]

Try #eval A or #reduce A?

[orlando]

reduce : give me indeterminate time out !
For #eval A

new.lean:17:0: warning
result type does not have an instance of type class 'has_repr', dumping internal representation
new.lean:17:0: information eval result
#0

[Reid Barton]

#eval A won't work because A has type ∃ s : R, ∃ N_f N_g : ℕ, f^(N_f+n) * s = f^N_f * s_f ∧ g^(N_g+n) * s = g^N_g * s_g (with some specific values substituted for the variables) and this is an ∃, so it's a prop. That means there is no data at "runtime".

[Reid Barton]

#reduce A might work in principle I guess, but I'm not surprised it doesn't work in practice.

[Reid Barton]

If you want to be able to use your proofs to compute directly with #eval, then you would need to change some or all of your ∃ into subtypes or sigma types or custom structures that contain the data you need to eventually arrive at the result 4.

[Reid Barton]

For example, rather than the prop ∃ u v : R, a * u + b * v = 1, you would want to work with a structure that contains u, v and the proof of a * u + b * v = 1

[orlando]

Ok, i try ! Thx !

[Reid Barton]

You'll also have to switch to def when the result is data (rather than a prop), and you may need to rearrange your definitions to put use earlier, and other changes. (Does use work to construct general structures?) Don't hesitate to ask questions if this way of using Lean is new to you.

[orlando]

hum for the moment i don't know if i start with :

structure Uni_2 {R : Type}(a b: R) [comm_ring R] :=
(u : R)(v : R)
(certificat : a * u + b * v = (1 : R))

or with

structure Uni_2 {R : Type}[comm_ring R] :=
(a b: R)
(u : R)(v : R)
(certificat : a * u + b * v = (1 : R))

[Reid Barton]

The first one. Think of it as a replacement for co_max, which is data instead of merely a proposition.

[orlando]

Okay, i thinck i understand ! I have to create other structure, for exemple : a structure for the condition :

(∃ m : ℕ, f^m * g^(n+m) * s_f = g^m * f^(n+m) * s_g)

[orlando]

thx Reid !!!

[orlando]

In fact, it's mathematicaly coherent ! Tomorow :D

parameters (f g : R)
structure localy_zero (a : R) extends  comax(f)(g) :=
(m : ℕ)(n : ℕ)
(proof: f^m * a = 0 ∧ g^n * a = 0)