Commit 2023-08-28 19:47 837c4ae2

View on Github →

chore: tidy various files (#6577)

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Colimits.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

modified theorem PrimeSpectrum.comap_inducing_of_surjective

deleted theorem PrimeSpectrum.pUnit

added theorem PrimeSpectrum.punit

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Comp.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Prod.lean

Modified Mathlib/Analysis/Convex/Cone/Basic.lean

added theorem Convex.mem_toCone'

deleted theorem Convex.mem_to_cone'

Modified Mathlib/Analysis/NormedSpace/MazurUlam.lean

added theorem IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero

added theorem IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm

deleted theorem IsometryEquiv.coe_to_real_linear_equiv_of_map_zero

deleted theorem IsometryEquiv.coe_to_real_linear_equiv_of_map_zero_symm

added theorem IsometryEquiv.toRealLinearIsometryEquiv_apply

deleted theorem IsometryEquiv.to_real_linear_equiv_apply

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.exists_ideal_over_prime_of_isIntegral'

deleted theorem Ideal.exists_ideal_over_prime_of_is_integral'

Modified Mathlib/Topology/VectorBundle/Basic.lean