feat(ring_theory/determinants): determinants #378
Conversation
|
Hm, |
|
I have removed |
data/fin.lean
Outdated
| apply fin.eq_of_veq, | ||
| by_cases h : i.val < pivot.val, | ||
| { simp [h] }, | ||
| { unfold ite dite, |
There was a problem hiding this comment.
uh, don't unfold ite and dite. Use split_ifs, or explicit rewrites using dif_pos etc...
data/fin.lean
Outdated
| @[simp] lemma lower_val (k : fin (n+1)) (H : k.1 < n) : (k.lower H).val = k.val := rfl | ||
|
|
||
| def ascend (pivot : fin (n+1)) : Π i : fin n, fin (n+1) := | ||
| λ i, if i.1 < pivot.1 then i.raise else i.succ |
There was a problem hiding this comment.
Why Π i : and not use the i? You can just move this before the :.
You can do this everywhere, at lower, descend, ...
ring_theory/determinants.lean
Outdated
| open equiv | ||
| variables {n : Type u} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R] | ||
|
|
||
| instance : group (equiv.perm n) := by apply_instance |
There was a problem hiding this comment.
I'm pretty sure this is already setup as a group.
ring_theory/determinants.lean
Outdated
| if H : i = j then by simp [H, equiv.swap_self] else | ||
| by simp [equiv.perm.sign_swap H, H] | ||
|
|
||
| def e (σ : equiv.perm n) : R := ((σ.sign : ℤ) : R) |
There was a problem hiding this comment.
You want to have e in the matrix namespace? It isn't even related to matices.
|
I've moved all sorts of helper lemmas to different files. This PR is starting to touch lots of basic files. I hope this is not a problem. |
|
Added in #404 |
|
This PR still has other stuff in it which wasn't merged with the other commit, it should be reorganized and PR'd again (or reopen this PR after rebasing on master) |
This PR depends on #374 and #375. In particular there is some code in
ring_theory/determinants.leanthat is currently commented out. This can be uncommented after the other two PR's are merged.TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list