Commit 2024-04-29 20:47 283ea7e3

View on Github →

chore(AdicCompletion): move to RingTheory and make folder (#12511) Move AdicCompletion from LinearAlgebra into its own folder in RingTheory as it seems to fit better there.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/LinearAlgebra/AdicCompletion.lean to Mathlib/RingTheory/AdicCompletion/Basic.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

Modified Mathlib/RingTheory/Henselian.lean