English
Equality with Nat.find under a predicate h defines ramificationIdx as the least n with the property.
Русский
Равенство с Nat.find через предикат h определяет ramificationIdx как наименьшее n, удовлетворяющее свойству.
LaTeX
$$$ramificationIdx f p P = Nat.find h$$$
Lean4
theorem ramificationIdx_comap_eq [Algebra R S] (e : S ≃ₐ[R] S₁) (P : Ideal S₁) :
ramificationIdx (algebraMap R S) p (P.comap e) = ramificationIdx (algebraMap R S₁) p P :=
by
dsimp only [ramificationIdx]
congr 1
ext n
simp only [Set.mem_setOf_eq, Ideal.map_le_iff_le_comap]
rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁), ← map_comap_of_equiv, ←
Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _), comap_comap, RingEquiv.symm_symm,
e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
