## Stream: maths

### Topic: Difference between is_prime and normal

#### Chris Hughes (Jun 06 2020 at 10:47):

Why does this work for prime ideals, but not normal subgroups?

import group_theory.subgroup ring_theory.ideal_operations

example {R : Type} [comm_ring R] (P : ideal R) (hP : P.is_prime) : P.is_prime :=
by apply_instance --works

example {G : Type} [group G] (N : subgroup G) (hN : N.normal) : N.normal :=
by apply_instance --fails


#### Chris Hughes (Jun 07 2020 at 08:49):

So it seems that the difference is that is_prime is a structure (and), but normal is not. The class attribute doesn't seem to work on defs defined to start with two pis, one pi is fine for some reason. Making normal irreducible also works.

This also doesn't work, so the fact idea might be slightly flawed.

example {P Q R : Prop} [fact (P → Q → R)] : fact (P → Q → R) := by apply_instance


#### Kevin Buzzard (Jun 07 2020 at 08:55):

This is the main reason that 1 isn't prime

#### Chris Hughes (Jun 07 2020 at 08:56):

Maybe top shouldn't be normal either and then everything will be fine

#### Mario Carneiro (Jun 07 2020 at 09:21):

That sounds like a bug in typeclass inference

#### Kevin Buzzard (Jun 07 2020 at 09:26):

top isn't prime but I'm afraid it's normal

lean#300

#### Kevin Buzzard (Jun 07 2020 at 11:00):

Lean is now about five times less relaxed

#### Reid Barton (Jun 07 2020 at 12:52):

Oh huh, I wonder whether this would fix some of the odd errors we used to get with limits in category theory as well.

#### Chris Hughes (Jun 07 2020 at 13:23):

Gabriel Ebner said:

lean#300

If this is released I can fix my PR.

Last updated: May 10 2021 at 07:15 UTC