English
The action of AlgEquiv K L L on primesOver p B is compatible with composition of automorphisms, i.e., (σ τ) • Q = σ • (τ • Q) for σ, τ.
Русский
Действие AlgEquiv K L L на primesOver p B совместимо с композициями автоморфизмов: (σ τ) • Q = σ • (τ • Q).
LaTeX
$$$(\\sigma \\tau) \\cdot Q = \\sigma \\cdot (\\tau \\cdot Q)$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Ideal.ramificationIdx]
public meta def
«_aux_Mathlib_NumberTheory_RamificationInertia_Unramified___delab_app__private_Mathlib_NumberTheory_RamificationInertia_Unramified_0_termE(_|_)_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 7
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Ideal.ramificationIdx)) (matchVar✝ `R))
pure✝)
pure✝)
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `algebraMap)) (matchVar✝ `R)) pure✝)
pure✝)
pure✝)
pure✝))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Ideal.under)) (matchVar✝ `R)) pure✝)
pure✝)
pure✝)
pure✝)
(matchVar✝ `P)))
(matchVar✝ `P) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ =>
MatchState.delabVar✝ s✝ `R (some✝ e✝) >>= fun R =>
MatchState.delabVar✝ s✝ `P (some✝ e✝) >>= fun P => withHeadRefIfTagAppFns✝ `(e($P|$R)))
