michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/theories/group_theory): remove dangling "check"s

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-16 22:50:02 -04:00
parent 9d83361fdc
commit c0cd72fc8d
2 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/theories/group_theory/hom.lean
View file

@ -36,7 +36,6 @@ definition is_hom (f : A → B) [h : is_hom_class f] : homomorphic f :=
@is_hom_class.is_hom A B s1 s2 f h @is_hom_class.is_hom A B s1 s2 f h
definition ker (f : A → B) [h : is_hom_class f] : set A := {a : A | f a = 1} definition ker (f : A → B) [h : is_hom_class f] : set A := {a : A | f a = 1}
check @ker
definition isomorphic (f : A → B) := injective f ∧ homomorphic f definition isomorphic (f : A → B) := injective f ∧ homomorphic f
structure is_iso_class [class] (f : A → B) extends is_hom_class f : Type := structure is_iso_class [class] (f : A → B) extends is_hom_class f : Type :=
@ -174,7 +173,6 @@ lemma ker_map_is_hom : homomorphic (ker_natural_map : coset_of (ker f) → B) :=
take aK bK, take aK bK,
quot.ind (λ a, quot.ind (λ b, ker_coset_hom a b) bK) aK quot.ind (λ a, quot.ind (λ b, ker_coset_hom a b) bK) aK
check @subg_in_lcoset_same_lcoset
lemma ker_coset_inj (a b : A) : (ker_natural_map ⟦a⟧ = ker_natural_map ⟦b⟧) → ⟦a⟧ = ⟦b⟧ := lemma ker_coset_inj (a b : A) : (ker_natural_map ⟦a⟧ = ker_natural_map ⟦b⟧) → ⟦a⟧ = ⟦b⟧ :=
assume Pfeq : f a = f b, assume Pfeq : f a = f b,
assert Painb : a ∈ b ∘> ker f, from calc assert Painb : a ∈ b ∘> ker f, from calc

1
library/theories/group_theory/perm.lean
View file

@ -42,7 +42,6 @@ end perm
structure perm (A : Type) [h : fintype A] : Type := structure perm (A : Type) [h : fintype A] : Type :=
(f : A → A) (inj : injective f) (f : A → A) (inj : injective f)
local attribute perm.f [coercion] local attribute perm.f [coercion]
check perm.mk
section perm section perm
variable {A : Type} variable {A : Type}