# Zulip Chat Archive

## 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 `pi`

s, 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

#### Gabriel Ebner (Jun 07 2020 at 10:31):

#### 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:

If this is released I can fix my PR.

Last updated: May 10 2021 at 07:15 UTC