subgroup

Stream: new members

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic

variable (G : Type _ ) [Group G]

structure my_subgroup (H : set G) extends subgroup G :=
(carrier_mem' : carrier = H)

I define subgroups like this and it reminds me 'type expected, got
(set G : ?m.17 PUnit)’, so how to correctly define subgroups?

[Kevin Buzzard]

Try switching on set_option autoImplicit false to see if the error changes?

[tsuki hao]

Kevin Buzzard said:

Try switching on set_option autoImplicit false to see if the error changes?

The error has not changed, it is still the original error

[Kevin Buzzard]

I'm surprised because stuff like set and subgroup should surely have capital letters in lean 4

[Mario Carneiro]

MonadStateOf.set.{u, v} {σ : semiOutParam (Type u)} {m : Type u → Type v} [self : MonadStateOf σ m] (a✝ : σ) : m PUnit

(that is, set G is defined, to mean "assign the state value of monad m to G", which is probably not what you want)

[Mario Carneiro]

subgroup isn't elaborated because of the earlier error, but if you use Set G then it gives the error you probably expected:

unknown identifier 'subgroup'
'sorryAx' is not a structure

[tsuki hao]

Kevin Buzzard said:

I'm surprised because stuff like set and subgroup should surely have capital letters in lean 4

Thank you very much!

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic

variable (G : Type _ ) [Group G]

set_option autoImplicit false

example (H₁ H₂ : Subgroup G) (h : have (H₁ ∪ H₂): Subgroup G) : H₁ ⊆ H₂ ∨ H₂ ⊆ H₁ := by
  sorry

Can I ask what is wrong with me describing H1 and H2 is still being subgroups

[Eric Wieser]

Please don't post the same question in two places

[Eric Wieser]

I answered in your other thread

[tsuki hao]

Eric Wieser said:

Please don't post the same question in two places

I am so sorry to bother you, I mistakenly thought I should reopen a topic

[Kyle Miller]

It's fine re-using a topic, but if you post the same question in two places it can lead to people independently answering your question without being aware of other answers. Eric's message is letting everyone else know not to leave any answers in this topic.