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

fix(library/theories/group_theory): have-tactic

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-29 12:13:53 -08:00
parent cc8d9bc7ff
commit 3b73b5b207
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/theories/group_theory/action.lean
View file

@ -431,7 +431,7 @@ subset_of_forall take g, begin
apply finsubg_has_inv,
apply mem_sep_of_mem !mem_univ,
intro h Ph,
have Phg : fin_lcoset (fin_lcoset H g) h = fin_lcoset H g, exact PH Ph,
have Phg : fin_lcoset (fin_lcoset H g) h = fin_lcoset H g, from PH Ph,
revert Phg,
rewrite [↑conj_by, inv_inv, mul.assoc, fin_lcoset_compose, -fin_lcoset_same, ↑fin_lcoset, mem_image_iff, ↑lmul_by],
intro Pex, cases Pex with k Pand, cases Pand with Pkin Pk,
@ -494,9 +494,8 @@ lemma lift_lower_eq : ∀ {p : perm (fin (succ n))} (P : p maxi = maxi),
| (perm.mk pf Pinj) := assume Pmax, begin
rewrite [↑lift_perm], congruence,
apply funext, intro i,
have Pfmax : pf maxi = maxi, apply Pmax,
have Pd : decidable (i = maxi),
exact _,
have Pfmax : pf maxi = maxi, by apply Pmax,
have Pd : decidable (i = maxi), from _,
cases Pd with Pe Pne,
rewrite [Pe, Pfmax], apply lift_fun_max,
rewrite [lift_fun_of_ne_max Pne, ↑lower_perm, ↑lift_succ],

6
library/theories/group_theory/cyclic.lean
View file

@ -194,9 +194,11 @@ lemma order_of_min_pow {a : A} {n : nat}
or.elim (eq_or_lt_of_le (order_le Pone)) (λ P, P)
(λ P : order a < succ n, begin
have Pn : a^(order a) ≠ 1,
begin
rewrite [-(succ_pred_of_pos (order_pos a))],
apply Pmin, apply nat.lt_of_succ_lt_succ,
rewrite [succ_pred_of_pos !order_pos], assumption,
rewrite [succ_pred_of_pos !order_pos], assumption
end,
exact absurd (pow_order a) Pn end)
lemma order_dvd_of_pow_eq_one {a : A} {n : nat} (Pone : a^n = 1) : order a ∣ n :=
@ -243,7 +245,7 @@ local attribute group_of_add_group [instance]
lemma pow_eq_mul {n : nat} {i : fin (succ n)} : ∀ {k : nat}, i^k = mk_mod n (i*k)
| 0 := by rewrite [pow_zero]
| (succ k) := begin
have Psucc : i^(succ k) = madd (i^k) i, apply pow_succ',
have Psucc : i^(succ k) = madd (i^k) i, by apply pow_succ',
rewrite [Psucc, pow_eq_mul],
apply eq_of_veq,
rewrite [mul_succ, val_madd, ↑mk_mod, mod_add_mod]