Theorems · Theorem · commutative algebra

StandardEtalePresentation.mk.congr_simp

∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P P_1 : StandardEtalePair R) (e_P : P = P_1) (x x_1 : S) (e_x : x = x_1) (hasMap : P.HasMap x)
  (lift_bijective : Function.Bijective ⇑(P.lift x hasMap)),
  { P := P, x := x, hasMap := hasMap, lift_bijective := lift_bijective } =
    { P := P_1, x := x_1, hasMap := ⋯, lift_bijective := ⋯ }

Defined in

Mathlib.RingTheory.Smooth.IntegralClosure

Cited by

0 results in Mathlib

Foundations

Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra