Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 25cf763

Browse files
VierkantorVierkantor
committed
chore(ring_theory): move submodule.fg to ring_theory.finiteness (#17541)
Theory on finitely generated submodules was defined in `ring_theory.noetherian`, but we can easily move it to `ring_theory.finiteness` which needs noticeably fewer imports. This move flips the import direction between the two files, since `finiteness` used to import `noetherian` and now it's the other way. Finally, some results that didn't fit neatly in either file are now in the new file `ring_theory.ideal.idempotent_fg`. As suggested in the discussion on #17481.
1 parent 8350c34 commit 25cf763

4 files changed

Lines changed: 469 additions & 438 deletions

File tree

‎src/linear_algebra/matrix/nonsingular_inverse.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -458,8 +458,7 @@ invertible.map (diagonal_ring_hom n α) v
458458

459459
lemma inv_of_diagonal_eq {α} [semiring α] (v : n → α) [invertible v] [invertible (diagonal v)] :
460460
⅟(diagonal v) = diagonal (⅟v) :=
461-
by { letI := diagonal_invertible v, convert (rfl : ⅟(diagonal v) = _),
462-
convert subsingleton.elim _ _, apply invertible.subsingleton }
461+
by { letI := diagonal_invertible v, convert (rfl : ⅟(diagonal v) = _) }
463462

464463
/-- `v` is invertible if `diagonal v` is -/
465464
def invertible_of_diagonal_invertible (v : n → α) [invertible (diagonal v)] : invertible v :=

0 commit comments

Comments
 (0)