English
If i: K →* L and f: L →* M are p-radical, then the composition f ∘ i: K →* M is also p-radical.
Русский
Если i: K → L и f: L → M являются p-радикальными гомоморфизмами, то их композиция f ∘ i: K → M также является p-радикальной.
LaTeX
$$$IsPRadical(f \\circ i, p)$$$
Lean4
/-- Composition of `p`-radical ring homomorphisms is also `p`-radical. -/
theorem trans [IsPRadical i p] [IsPRadical f p] : IsPRadical (f.comp i) p
where
pow_mem'
x := by
obtain ⟨n, y, hy⟩ := pow_mem f p x
obtain ⟨m, z, hz⟩ := pow_mem i p y
exact ⟨n + m, z, by rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]⟩
ker_le' x
h := by
rw [RingHom.mem_ker, RingHom.comp_apply, ← RingHom.mem_ker] at h
simpa only [← Ideal.mem_comap, comap_pNilradical] using ker_le f p h
