Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…mathlib4 into interval_instances

…v program (#6284)

The Cache program after detecting that LeanTar is old downloads it and attempts to place it in the `CACHEDIR` directory. It then attempts to rename it using the `mv` command it assumes is present on the platform. On windows `cmd` and `powershell` this does not work since `mv` is actually a shell built in and not an executable. (This will however work on MinGW based shells).

@digama0 added the function `IO.FS.rename` in Lean [Lean4#2345](leanprover/lean4#2345 (comment)) which calls the standard C/C++ function `rename`. This PR uses this function to move leantar instead of the runCmd command. When this fix succeeds the output looks like the following (in powershell).

```text
PS W:\LeanStuff\graveyard_mathlib4\LeanCacheFix> lake exe cache get
leantar is too old; downloading more recent version
Attempting to download 3614 file(s)
Downloaded: 3614 file(s) [attempted 3614/3614 = 100%] (100% success)
Decompressing 3614 file(s)
unpacked in 323 ms
```



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Add the following result: 
```lean
theorem mem_span_integralBasis {x : K} :
    x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K
```
that is, `integralBasis` is indeed a `ℤ`-basis of the ring of integers. 

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>



Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

This was done once in #5063, then accidentally reverted in #5859.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as `A = fromColumns A₁ A₂` the concatenation of two matrices with the same column indices can be expressed as `B = fromRows B₁ B₂`.

We then provide a few lemmas that deal with the products of these with each other and with block matrices. Two particular lemmas `fromColumns_mul_fromRows_eq_one_comm` and `equiv_compl_fromColumns_mul_fromRows_eq_one_comm` deal with the case of matrix multiplication that gives one as a result. This gives a crude (but usable) replacement for the `Invertible` type which can only be applied to square matrices (with the same index type for rows and columns).

Found while doing a larger refactor. This doesn't change any defeqs, and the new proofs make it obvious that there's nothing interesting going on here.

Fixes an issue [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60lake.20exe.20cache.20get.60.20fails.20in.20command.20prompt/near/377455000).

… n` (#6292)

This PR replaces `Fact ((n : ℕ) % 2 = 1)` with `Odd n`, as suggested in #6086.

…ic (#4595)

This is a first PR porting some of the functionality of the `extract_goal` tactic from mathlib3.



Co-authored-by: Alex J Best <alex.j.best@gmail.com>

…independence (#6294)

Independence is the special case of independence with respect to a kernel and a measure where the kernel is constant.

Modify `tauto` to throw an error message "tauto failed to solve some goals" if it fails.

This generalizes from `Algebra.lsmul R M : A →ₐ[R] Module.End R M` to `Algebra.lsmul R S M : A →ₐ[R] Module.End S M`.

This generalization was previously not possible because `Module.End S M` was not an `R`-algebra.

Notably this now allows things like `Algebra.lsmul R A A : Aᵐᵒᵖ →ₐ[R] Module.End A A` (right multiplication).

This doesn't bother attempting to generalize uses in downstream files, as most of them probably do not need the generality.
Instead, we just replace `Algebra.lsmul R` with `Algebra.lsmul R R`.

An R-derivation from `R[X]` is determined by its value on `X`. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed `MvPolynomial.Derivation` .




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

…Equiv` (#6305)

This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`. The motivation is to make room for `QuadraticForm.Isometry` as the homomorphism.

…6314)

This is easier to remove from the `classical` locale in future, and is arguably more readable

This removes the `with` pattern from the `Field` and `CommSemiGroupWithZero` instances on `Rat`.

The resulting term decreases in size by an order of magnitude (at least).



Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

We define the torsion subgroup of the units of a number field and prove some results about it, mostly: it is finite, cyclic and 
an unit is torsion iff its value is 1 at all infinite places. Some results linking to `rootsOfUnity` are also proved. 

This PR also includes a direct coercion from `(𝓞 K)ˣ` to `K` that is very convenient, although I am not sure it's done properly.