English
If h is IsAdjoinRootMonic S f, then the powerBasis h is a PowerBasis with generator h.root, dimension natDegree f, basis h.basis, and basis_eq_pow given by h.basis_apply.
Русский
Пусть h — IsAdjoinRootMonic S f; тогда powerBasis(h) — это базис степени с генератором h.root, размерностью natDegree f, базисом h.basis и равенством basis_eq_pow, задаваемым h.basis_apply.
LaTeX
$$$\\text{powerBasis}(h) : PowerBasis\\, R\\, S \\; \\text{with} \\; \\text{gen}=h.root,\\ \\text{dim}=\\operatorname{natDegree} f,\\ \\text{basis}=h.basis,\\ \\text{basis\\_eq\\_pow}=h.basis\\_apply$$$
Lean4
/-- If `f` is monic, the powers of `h.root` form a basis. -/
@[simps! gen dim basis]
def powerBasis : PowerBasis R S where
gen := h.root
dim := natDegree f
basis := h.basis
basis_eq_pow := h.basis_apply
