Theorems · Theorem · commutative algebra

Algebra.PreSubmersivePresentation.jacobian_reindex

∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ)
  [inst_3 : Finite σ] [inst_4 : Finite σ'], (P.reindex e f).jacobian = P.jacobian

Defined in

Mathlib.RingTheory.Extension.Presentation.Submersive

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFiniteFinite