FLT/Patching/REqualsT.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

R = T from a successful patching argument

The final step of the patching argument: under the relevant hypotheses, the kernel of the surjection R → T is contained in the nilradical, so the map R → T is an isomorphism after passing to reduced quotients.

Imports (1)
Imported by 1 file
  1. theorem ker_RtoT_le_nilradical line 86 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, IsNoetherianRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, Algebra, AddCommGroup, Nontrivial, Module, IsScalarTower, Ultrafilter, Algebra.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem and 28 more

    Proof uses: Module.Finite, IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Or.inl, False, Filter.NeBot.ne', Subsingleton.elim, Filter, Bot.bot, Eq.refl, Or.inr, Nonempty.some, inferInstance, Module.Finite.equiv, Module.Finite.of_restrictScalars_finite, Eq.mpr, Ideal.radical, OfNat.ofNat and 30 more

    170 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

    Open to load the checked before-and-after goal states.