Commit 2024-06-13 02:15 495396de

View on Github →

chore: split Mathlib.Data.Complex.Module (#13762)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/AbelLimit.lean

Modified Mathlib/Analysis/Complex/Conformal.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Analysis/PSeriesComplex.lean

Modified Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

Created Mathlib/Data/Complex/FiniteDimensional.lean

added theorem Complex.finrank_real_complex

added theorem Complex.finrank_real_complex_fact

added theorem Complex.nonempty_linearEquiv_real

added theorem Complex.rank_rat_complex

added theorem Complex.rank_real_complex'.{u}

added theorem Complex.rank_real_complex

added theorem Real.rank_rat_real

added theorem finrank_real_of_complex

added theorem rank_real_of_complex

Modified Mathlib/Data/Complex/Module.lean

deleted theorem Complex.finrank_real_complex

deleted theorem Complex.finrank_real_complex_fact

deleted theorem Complex.nonempty_linearEquiv_real

deleted theorem Complex.rank_rat_complex

deleted theorem Complex.rank_real_complex'.{u}

deleted theorem Complex.rank_real_complex

deleted theorem Real.rank_rat_real

deleted theorem finrank_real_of_complex

deleted theorem rank_real_of_complex

Modified Mathlib/NumberTheory/LSeries/Basic.lean

Modified Mathlib/Topology/Instances/Complex.lean