English
If R<x> and R<y> generate the same subalgebra of S, then conductors of x and y are equal.
Русский
Если подалгебры, порождаемые x и y, совпадают, то conductor(R,x) = conductor(R,y).
LaTeX
$$$(R = R) \\Rightarrow \\mathrm{conductor}(R,x) = \\mathrm{conductor}(R,y)$$$
Lean4
/-- Let `S / R` be a ring extension and `x : S`, then the conductor of `R<x>` is the
biggest ideal of `S` contained in `R<x>`. -/
def conductor (x : S) : Ideal S where
carrier := {a | ∀ b : S, a * b ∈ R<x>}
zero_mem' b := by simp only [zero_mul, zero_mem]
add_mem' ha hb c := by simpa only [add_mul] using Subalgebra.add_mem _ (ha c) (hb c)
smul_mem' c a ha b := by simpa only [smul_eq_mul, mul_left_comm, mul_assoc] using ha (c * b)
