Kronecker's construction in interactive theorem provers?

Do you know good and user-friendly programs to measure plant quantitative traits?

For my research i will need to measure plant quantitative traits (especially leaves area and roots length, but would be nice to add some more information). I recently discovered...

01 March 2021 5,035 2 View

Good morning research fellows, Has anyone worked with senna alata plant extract on any kind of fish?

Literatures on the piscicidal effect of sennaa alata is scanty. if you have any related litrature either in the bark, leaves or roots used as treatment to any aquatic organism please kindly help...

28 February 2021 9,138 2 View

How to find the right number of integration points in second order 3d finite elements?

I am familiar with finite element simulations and numerical schemes like the Gauss Legendre quadrature. I also know that the Gauss integration yields exact values for polynomials up to degree 2n-1...

27 February 2021 6,818 3 View

Which microtomy technique do you suggest for thin and delicate root sectioning ?And, how to preserve and process the roots before sectioning?

We have thin roots of from 1 year old different species of plants. We are looking into anatomical details of the roots. What's the best method to preserve and process the roots once they are...

23 February 2021 1,898 1 View

How can we determine the positive definiteness of multivariable polyomial? Is there any MATLAB function available for that?

Can we check the positive definiteness of a multivariable polynomial using MATLAB functions? Of course in literature, there are few complex methods that use tensor algebra. However, before going...

16 February 2021 1,218 3 View

Which root in this tap root system, in the picture attached, should be used for root sectioning in order to study the root anatomical details?

There are numerous roots in this tap root system. Kindly suggest or share a research paper where I can clarify the doubts as to which root should be chosen for sectioning and for further root...

14 February 2021 1,816 3 View

Infinite order of Laguerre?

If Lmn(x) is the Laguerre polynomial of order m and degree n Is there a means of computing Lmn(x) for 1) m goes to infinity 2) n goes to infinity

08 February 2021 6,320 4 View

Is there any research Mathematical perceptions depending on type of personalities?

My dissertation thesis is Perceptions of mathematical ceonceptions depending on Myers-Briggs Type Indicator personalities. It can includes methods of solving, understanding, imaginations of math...

07 February 2021 9,880 4 View

What is the relationship that determines the depth of the mechanical cultivator with the age or size of the weed For crops planted in lines?

the great depth of the cultivator may lead to passage under the roots without killing them and may give negative results to break up the soil below the roots, increasing their activity, especially...

03 February 2021 3,198 7 View

Why do high doses of humic substances inhibit the growth of corn roots? Is there a toxicity effect?

Length, volume, surface area and dry mass of corn roots treated with humic substances increased up to 13 liters per hectare and decreased with higher doses.

02 February 2021 2,190 4 View

Shuker Khalil

I think you need to explain which field extension Q[sqrt(b)] you mean for any b or for some b you found A[sqrt(b)] is Isabelle. Thanks

Christoph Schwarzweller

Dear Shuker,

thanks for your answer. I wnat to prove the general version, that is the following.

Let F be a field and p in F[X]\F an irreducible polynomial over F. Then there exists a field extension E of F, in which p has a root.

The standard proof uses F[X]\

as the field extension E.

In Isabelle I found Q[sqrt(b)] "for some fixed natural number b". That would be

Q[X]/ in the above setting, but probably it is implemented straightforwardly as { p + q * sqrt(b) } for rational number p and q?

Best regards

Christoph

Tapas Chatterjee

You may consider the splitting field of p over F.