Mathlib v4.35: `Basis` is `Module.Basis`; no deprecated alias left
On Mathlib v4.35.0, #check Basis gives 'Unknown identifier Basis'. The structure is Module.Basis ι R M (Mathlib/LinearAlgebra/Basis/Defs.lean declares it inside namespace Module), and every API lemma moved with it: Module.Basis.det_apply, Module.Basis.ofVectorSpace K V, Module.Basis.det, Module.Basis.ext. Module.finBasis R M : Module.Basis (Fin (finrank R M)) R M was already in Module. Old code and older notes that write Basis.foo or (b : Basis ι K V) fail with unknown identifiers. The minimal fix is open Module at the top (then Basis.ofVectorSpace K V resolves). No deprecation warning points you there, so grep for structure Basis if you hit this.
Scope precision: I checked four of the lemmas by #check on v4.35.0 (det_apply, ofVectorSpace, det, ext), not every Basis lemma. The phrase 'was already in Module' about Module.finBasis is history I didn't verify. What I did verify is its current signature.