power_in_kernel_of_finite_image

Stream: new members

[Shara Hunt]

import Mathlib.GroupTheory.OrderOfElement

import Mathlib.Algebra.Group.Subgroup.Basic

import Mathlib.Data.Fintype.Basic

import Mathlib.Data.Fintype.Card

import Mathlib.Data.Set.Finite.Basic

open Function

theorem power_in_kernel_of_finite_image

{G H : Type*} [Group G] [Group H]

(f : G →* H) (hf : (Set.range f).Finite) :

∀ x : G, ∃ n : ℕ, x ^ n ∈ f.ker := by

intro x

let K := Subgroup.closure (Set.range f)

-- 给出 Fintype 实例

have hK : Set.Finite (K : Set H) := Subgroup.closure_closure_coe_preimage

letI : Fintype K := Fintype.ofFinite _

-- 构造 f x 属于 K 中的元素

have hx : f x ∈ K := Subgroup.subset_closure (Set.mem_range_self x)

let y : K := ⟨f x, hx⟩

-- 得到 f x 在 K 中阶整除阶数

have hpow : y ^ Fintype.card K = 1 := pow_card_eq_one y

-- 拆掉 coercion 包装

simp only [Subgroup.coe_pow, Subgroup.coe_one, Subgroup.coe_mk] at hpow

-- 最终结论

use Fintype.card K

rw [MonoidHom.mem_ker, map_pow]

exact hpow请问这个怎么解决啊，ll Messages (4)

EX05.lean:17:38

type mismatch
Subgroup.closure_closure_coe_preimage
has type
Subgroup.closure (Subtype.val ⁻¹' ?m.759) = ⊤ : Prop
but is expected to have type
(↑K).Finite : Prop

EX05.lean:18:22

failed to synthesize
Finite ↥K

Additional diagnostic information may be available using the set_option diagnostics true command.

EX05.lean:25:40

function expected at
pow_card_eq_one
term has type
?m.1895 ^ Fintype.card ?m.1892 = 1

EX05.lean:33:2

type mismatch
hpow
has type
y ^ Fintype.card ↥K = 1 : Prop
but is expected to have type
f x ^ Fintype.card ↥K = 1 : Prop

Restart File，

[Ruben Van de Velde]

You'll need to use #backticks to make that readable

[Notification Bot]

This topic was moved here from #lean4 > native support of coinductive types / codata by Kevin Buzzard.

[Notification Bot]

3 messages were moved here from #new members > native support of coinductive types / codata by Matt Diamond.